Constructing a formal proof of certain logical arguments Given the following arguments:
$ \tag A (R \to \neg S) \land  (T \to \neg U)$
$ \tag B (V\to \neg W) \land  (X \to \neg Y)$
$ \tag C (T \to  W) \land  (U \to  S)$
$ \tag D V \lor R $
$$ \therefore \neg T \lor \neg U $$
how to prove  this using the standard rules of inference?
 A: One expects this to follow more or less  directly from $(A)$ because $p\to q\iff \neg p \lor q$.
However, there is no tertium no datur.
One has to find ones luch starting from (D) by case analysis:
By simplification from (A):
$$\tag{1}R\to\neg S$$
and 
$$\tag2 T\to\neg U$$
By simplification from (C):
$$\tag{3}T\to W$$
and 
$$\tag4 U\to S$$
By modus ponens from (1):
$$\tag 5R\vdash \neg S$$
By modus tollens from  (4) and (5):
$$\tag 6 R\vdash \neg U$$
By addition from (6)
$$\tag 7 R\vdash \neg T \lor \neg U$$
By decuction theorem from (6):
$$\tag 8 R\to (\neg T \lor \neg U)$$
By simplification from (B):
$$\tag 9 V\to\neg W$$
By modus ponens from (9):
$$\tag{10} V\vdash \neg W$$
By modus tollens from (10) and (3):
$$\tag{11}V\vdash \neg T$$
By addition from (11):
$$\tag{12}V\vdash \neg T\lor\neg U$$
By deduction theorem from (12)
$$\tag{13}V\to( \neg T\lor\neg U)$$
By case analysis from (D), (13) and (8):
$$\neg T \lor \neg U_\blacksquare$$
A: Here is a proof using a Fitch-style proof checker:

The first four lines state the premises. I then attempt to consider both cases in premise 4 by assuming each in a subproof and deriving the desired goal. When that is done I can use disjunction elimination or case analysis (vE) on line 17 to complete the proof.
Within the subproofs I used conjunction elimination or simplification (∧E), conditional elimination or modus ponens (→E), disjunction introduction or addition (vI) and modus tollens (MT).
All rules are listed on the OP's rules of inference.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
