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  8333  sdomdomtr  9030  domsdomtr  9032  infdif  10106  ackbij1b  10136  isf32lem5  10255  alephreg  10480  cfpwsdom  10482  inar1  10673  tskcard  10679  npomex  10894  recnz  12554  rpnnen1lem5  12881  fznuz  13511  uznfz  13512  seqcoll2  14374  ramub1lem1  16940  chnccat  18534  pgpfac1lem1  19990  lsppratlem6  21091  nconnsubb  23339  iunconnlem  23343  clsconn  23346  xkohaus  23569  reconnlem1  24743  ivthlem2  25381  perfectlem1  27168  lgseisenlem1  27314  ex-natded5.8-2  30396  oddpwdc  34388  erdszelem9  35264  relowlpssretop  37429  sucneqond  37430  heiborlem8  37878  lcvntr  39145  ncvr1  39391  llnneat  39633  2atnelpln  39663  lplnneat  39664  lplnnelln  39665  3atnelvolN  39705  lvolneatN  39707  lvolnelln  39708  lvolnelpln  39709  lplncvrlvol  39735  4atexlemntlpq  40187  cdleme0nex  40409  nlimsuc  43558