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  8383  sdomdomtr  9086  domsdomtr  9088  infdif  10179  ackbij1b  10209  isf32lem5  10329  alephreg  10555  cfpwsdom  10557  inar1  10748  tskcard  10754  npomex  10969  recnz  12662  rpnnen1lem5  12996  fznuz  13628  uznfz  13629  seqcoll2  14492  ramub1lem1  17076  chnccat  18672  pgpfac1lem1  20137  lsppratlem6  21245  nconnsubb  23541  iunconnlem  23545  clsconn  23548  xkohaus  23771  reconnlem1  24945  ivthlem2  25572  perfectlem1  27351  lgseisenlem1  27497  ex-natded5.8-2  30674  oddpwdc  34661  fineqvinfep  35433  erdszelem9  35562  relowlpssretop  37870  sucneqond  37871  heiborlem8  38329  lcvntr  39662  ncvr1  39908  llnneat  40150  2atnelpln  40180  lplnneat  40181  lplnnelln  40182  3atnelvolN  40222  lvolneatN  40224  lvolnelln  40225  lvolnelpln  40226  lplncvrlvol  40252  4atexlemntlpq  40704  cdleme0nex  40926  nlimsuc  44029