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  8027  sdomdomtr  8634  domsdomtr  8636  infdif  9620  ackbij1b  9650  isf32lem5  9768  alephreg  9993  cfpwsdom  9995  inar1  10186  tskcard  10192  npomex  10407  recnz  12045  rpnnen1lem5  12368  fznuz  12984  uznfz  12985  seqcoll2  13819  ramub1lem1  16352  pgpfac1lem1  19189  lsppratlem6  19917  nconnsubb  22028  iunconnlem  22032  clsconn  22035  xkohaus  22258  reconnlem1  23431  ivthlem2  24056  perfectlem1  25813  lgseisenlem1  25959  ex-natded5.8-2  28199  oddpwdc  31722  erdszelem9  32559  relowlpssretop  34781  sucneqond  34782  heiborlem8  35256  lcvntr  36322  ncvr1  36568  llnneat  36810  2atnelpln  36840  lplnneat  36841  lplnnelln  36842  3atnelvolN  36882  lvolneatN  36884  lvolnelln  36885  lvolnelpln  36886  lplncvrlvol  36912  4atexlemntlpq  37364  cdleme0nex  37586