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  8327  sdomdomtr  9023  domsdomtr  9025  infdif  10096  ackbij1b  10126  isf32lem5  10245  alephreg  10470  cfpwsdom  10472  inar1  10663  tskcard  10669  npomex  10884  recnz  12545  rpnnen1lem5  12876  fznuz  13506  uznfz  13507  seqcoll2  14369  ramub1lem1  16935  chnccat  18529  pgpfac1lem1  19986  lsppratlem6  21087  nconnsubb  23336  iunconnlem  23340  clsconn  23343  xkohaus  23566  reconnlem1  24740  ivthlem2  25378  perfectlem1  27165  lgseisenlem1  27311  ex-natded5.8-2  30389  oddpwdc  34362  erdszelem9  35231  relowlpssretop  37397  sucneqond  37398  heiborlem8  37857  lcvntr  39064  ncvr1  39310  llnneat  39552  2atnelpln  39582  lplnneat  39583  lplnnelln  39584  3atnelvolN  39624  lvolneatN  39626  lvolnelln  39627  lvolnelpln  39628  lplncvrlvol  39654  4atexlemntlpq  40106  cdleme0nex  40328  nlimsuc  43473