Theorem mt2d 136

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 134	. 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  137  nsyl3  138  tz7.44-3  8344  sdomdomtr  9045  domsdomtr  9047  infdif  10128  ackbij1b  10158  isf32lem5  10277  alephreg  10503  cfpwsdom  10505  inar1  10696  tskcard  10702  npomex  10917  recnz  12602  rpnnen1lem5  12929  fznuz  13561  uznfz  13562  seqcoll2  14425  ramub1lem1  16995  chnccat  18590  pgpfac1lem1  20049  lsppratlem6  21152  nconnsubb  23413  iunconnlem  23417  clsconn  23420  xkohaus  23643  reconnlem1  24817  ivthlem2  25444  perfectlem1  27217  lgseisenlem1  27363  ex-natded5.8-2  30509  oddpwdc  34545  fineqvinfep  35313  erdszelem9  35434  relowlpssretop  37733  sucneqond  37734  heiborlem8  38192  lcvntr  39525  ncvr1  39771  llnneat  40013  2atnelpln  40043  lplnneat  40044  lplnnelln  40045  3atnelvolN  40085  lvolneatN  40087  lvolnelln  40088  lvolnelpln  40089  lplncvrlvol  40115  4atexlemntlpq  40567  cdleme0nex  40789  nlimsuc  43892