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  8408  sdomdomtr  9110  domsdomtr  9112  infdif  10204  ackbij1b  10234  isf32lem5  10352  alephreg  10577  cfpwsdom  10579  inar1  10770  tskcard  10776  npomex  10991  recnz  12637  rpnnen1lem5  12965  fznuz  13583  uznfz  13584  seqcoll2  14426  ramub1lem1  16959  pgpfac1lem1  19944  lsppratlem6  20765  nconnsubb  22927  iunconnlem  22931  clsconn  22934  xkohaus  23157  reconnlem1  24342  ivthlem2  24969  perfectlem1  26732  lgseisenlem1  26878  ex-natded5.8-2  29667  oddpwdc  33353  erdszelem9  34190  relowlpssretop  36245  sucneqond  36246  heiborlem8  36686  lcvntr  37896  ncvr1  38142  llnneat  38385  2atnelpln  38415  lplnneat  38416  lplnnelln  38417  3atnelvolN  38457  lvolneatN  38459  lvolnelln  38460  lvolnelpln  38461  lplncvrlvol  38487  4atexlemntlpq  38939  cdleme0nex  39161  nlimsuc  42192