Theorem mt2d 134

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 132	. 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  135  nsyl3  136  tz7.44-3  7775  sdomdomtr  8368  domsdomtr  8370  infdif  9353  ackbij1b  9383  isf32lem5  9501  alephreg  9726  cfpwsdom  9728  inar1  9919  tskcard  9925  npomex  10140  recnz  11787  rpnnen1lem5  12110  fznuz  12723  uznfz  12724  seqcoll2  13545  ramub1lem1  16108  pgpfac1lem1  18834  lsppratlem6  19520  nconnsubb  21604  iunconnlem  21608  clsconn  21611  xkohaus  21834  reconnlem1  23006  ivthlem2  23625  perfectlem1  25374  lgseisenlem1  25520  ex-natded5.8-2  27825  oddpwdc  30957  erdszelem9  31723  relowlpssretop  33752  sucneqond  33753  heiborlem8  34154  lcvntr  35096  ncvr1  35342  llnneat  35584  2atnelpln  35614  lplnneat  35615  lplnnelln  35616  3atnelvolN  35656  lvolneatN  35658  lvolnelln  35659  lvolnelpln  35660  lplncvrlvol  35686  4atexlemntlpq  36138  cdleme0nex  36360