Theorem mt2d 138

Description: Modus tollens deduction. (Contributed by NM, 4-Jul-1994.)

Hypotheses

Ref	Expression
mt2d.1	⊢ (𝜑 → 𝜒)
mt2d.2	⊢ (𝜑 → (𝜓 → ¬ 𝜒))

Assertion

Ref	Expression
mt2d	⊢ (𝜑 → ¬ 𝜓)

Proof of Theorem mt2d

Step	Hyp	Ref	Expression
1		mt2d.1	. 2 ⊢ (𝜑 → 𝜒)
2		mt2d.2	. . 3 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
3	2	con2d 136	. 2 ⊢ (𝜑 → (𝜒 → ¬ 𝜓))
4	1, 3	mpd 15	1 ⊢ (𝜑 → ¬ 𝜓)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  mt2i  139  nsyl3  140  tz7.44-3  8073  sdomdomtr  8700  domsdomtr  8702  infdif  9709  ackbij1b  9739  isf32lem5  9857  alephreg  10082  cfpwsdom  10084  inar1  10275  tskcard  10281  npomex  10496  recnz  12138  rpnnen1lem5  12463  fznuz  13080  uznfz  13081  seqcoll2  13917  ramub1lem1  16462  pgpfac1lem1  19315  lsppratlem6  20043  nconnsubb  22174  iunconnlem  22178  clsconn  22181  xkohaus  22404  reconnlem1  23578  ivthlem2  24204  perfectlem1  25965  lgseisenlem1  26111  ex-natded5.8-2  28351  oddpwdc  31891  erdszelem9  32732  relowlpssretop  35158  sucneqond  35159  heiborlem8  35599  lcvntr  36663  ncvr1  36909  llnneat  37151  2atnelpln  37181  lplnneat  37182  lplnnelln  37183  3atnelvolN  37223  lvolneatN  37225  lvolnelln  37226  lvolnelpln  37227  lplncvrlvol  37253  4atexlemntlpq  37705  cdleme0nex  37927