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  8044  sdomdomtr  8650  domsdomtr  8652  infdif  9631  ackbij1b  9661  isf32lem5  9779  alephreg  10004  cfpwsdom  10006  inar1  10197  tskcard  10203  npomex  10418  recnz  12058  rpnnen1lem5  12381  fznuz  12990  uznfz  12991  seqcoll2  13824  ramub1lem1  16362  pgpfac1lem1  19196  lsppratlem6  19924  nconnsubb  22031  iunconnlem  22035  clsconn  22038  xkohaus  22261  reconnlem1  23434  ivthlem2  24053  perfectlem1  25805  lgseisenlem1  25951  ex-natded5.8-2  28193  oddpwdc  31612  erdszelem9  32446  relowlpssretop  34648  sucneqond  34649  heiborlem8  35111  lcvntr  36177  ncvr1  36423  llnneat  36665  2atnelpln  36695  lplnneat  36696  lplnnelln  36697  3atnelvolN  36737  lvolneatN  36739  lvolnelln  36740  lvolnelpln  36741  lplncvrlvol  36767  4atexlemntlpq  37219  cdleme0nex  37441