Theorem mt2d 137

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 135	. 2 ⊢ (𝜑 → (𝜒 → ¬ 𝜓))
4	1, 3	mpd 16	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  138  nsyl3  139  tz7.44-3  8396  sdomdomtr  9099  domsdomtr  9101  infdif  10192  ackbij1b  10222  isf32lem5  10342  alephreg  10568  cfpwsdom  10570  inar1  10761  tskcard  10767  npomex  10982  recnz  12672  rpnnen1lem5  13006  fznuz  13639  uznfz  13640  seqcoll2  14504  ramub1lem1  17087  chnccat  18683  pgpfac1lem1  20147  lsppratlem6  21257  nconnsubb  23561  iunconnlem  23565  clsconn  23568  xkohaus  23791  reconnlem1  24965  ivthlem2  25592  perfectlem1  27371  lgseisenlem1  27517  ex-natded5.8-2  30743  oddpwdc  34722  fineqvinfep  35516  erdszelem9  35669  relowlpssretop  37988  sucneqond  37989  heiborlem8  38447  lcvntr  39778  ncvr1  40024  llnneat  40266  2atnelpln  40296  lplnneat  40297  lplnnelln  40298  3atnelvolN  40338  lvolneatN  40340  lvolnelln  40341  lvolnelpln  40342  lplncvrlvol  40368  4atexlemntlpq  40820  cdleme0nex  41042  nlimsuc  44147