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  8448  sdomdomtr  9150  domsdomtr  9152  infdif  10248  ackbij1b  10278  isf32lem5  10397  alephreg  10622  cfpwsdom  10624  inar1  10815  tskcard  10821  npomex  11036  recnz  12693  rpnnen1lem5  13023  fznuz  13649  uznfz  13650  seqcoll2  14504  ramub1lem1  17064  pgpfac1lem1  20094  lsppratlem6  21154  nconnsubb  23431  iunconnlem  23435  clsconn  23438  xkohaus  23661  reconnlem1  24848  ivthlem2  25487  perfectlem1  27273  lgseisenlem1  27419  ex-natded5.8-2  30433  oddpwdc  34356  erdszelem9  35204  relowlpssretop  37365  sucneqond  37366  heiborlem8  37825  lcvntr  39027  ncvr1  39273  llnneat  39516  2atnelpln  39546  lplnneat  39547  lplnnelln  39548  3atnelvolN  39588  lvolneatN  39590  lvolnelln  39591  lvolnelpln  39592  lplncvrlvol  39618  4atexlemntlpq  40070  cdleme0nex  40292  nlimsuc  43454