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  8347  sdomdomtr  9048  domsdomtr  9050  infdif  10130  ackbij1b  10160  isf32lem5  10279  alephreg  10505  cfpwsdom  10507  inar1  10698  tskcard  10704  npomex  10919  recnz  12604  rpnnen1lem5  12931  fznuz  13563  uznfz  13564  seqcoll2  14427  ramub1lem1  16997  chnccat  18592  pgpfac1lem1  20051  lsppratlem6  21150  nconnsubb  23388  iunconnlem  23392  clsconn  23395  xkohaus  23618  reconnlem1  24792  ivthlem2  25419  perfectlem1  27192  lgseisenlem1  27338  ex-natded5.8-2  30484  oddpwdc  34498  fineqvinfep  35269  erdszelem9  35381  relowlpssretop  37680  sucneqond  37681  heiborlem8  38139  lcvntr  39472  ncvr1  39718  llnneat  39960  2atnelpln  39990  lplnneat  39991  lplnnelln  39992  3atnelvolN  40032  lvolneatN  40034  lvolnelln  40035  lvolnelpln  40036  lplncvrlvol  40062  4atexlemntlpq  40514  cdleme0nex  40736  nlimsuc  43868