Theorem mt3d 148

Description: Modus tollens deduction. (Contributed by NM, 26-Mar-1995.)

Hypotheses

Ref	Expression
mt3d.1	⊢ (𝜑 → ¬ 𝜒)
mt3d.2	⊢ (𝜑 → (¬ 𝜓 → 𝜒))

Assertion

Ref	Expression
mt3d	⊢ (𝜑 → 𝜓)

Proof of Theorem mt3d

Step	Hyp	Ref	Expression
1		mt3d.1	. 2 ⊢ (𝜑 → ¬ 𝜒)
2		mt3d.2	. . 3 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
3	2	con1d 145	. 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:  mt3i  149  olcnd  874  ecase23d  1472  disjss3  5092  nnsuc  7799  frrlem14  8186  unxpdomlem2  9117  oismo  9398  cnfcom3lem  9561  rankelb  9682  fin33i  10227  isf34lem4  10235  canthp1lem2  10511  gchdju1  10514  pwfseqlem3  10518  inttsk  10632  r1tskina  10640  nqereu  10787  zbtwnre  12788  discr1  14056  seqcoll2  14280  bitsfzo  16242  bitsf1  16253  eucalglt  16388  4sqlem17  16760  4sqlem18  16761  ramubcl  16817  psgnunilem5  19199  odnncl  19250  gexnnod  19290  sylow1lem1  19300  torsubg  19551  prmcyg  19591  ablfacrplem  19764  pgpfac1lem2  19774  pgpfac1lem3a  19775  pgpfac1lem3  19776  xrsdsreclblem  20751  prmirredlem  20801  ppttop  22264  pptbas  22265  regr1lem  22997  alexsublem  23302  reconnlem1  24096  metnrmlem1a  24128  vitalilem4  24882  vitalilem5  24883  itg2gt0  25032  rollelem  25260  lhop1lem  25284  coefv0  25516  plyexmo  25580  lgamucov  26294  ppinprm  26408  chtnprm  26410  lgsdir  26587  lgseisenlem1  26630  2sqlem7  26679  2sqblem  26686  pntpbnd1  26841  dfon2lem8  34051  poxp2  34074  poxp3  34080  madebdaylemlrcut  34189  poimirlem25  35958  fdc  36059  ac6s6  36486  2atm  37846  llnmlplnN  37858  trlval3  38506  cdleme0moN  38544  cdleme18c  38612  qirropth  41043  aacllem  46923