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  878  disjss3  5084  nnsuc  7835  poxp2  8093  frrlem14  8249  unxpdomlem2  9167  oismo  9455  cnfcom3lem  9624  rankelb  9748  fin33i  10291  isf34lem4  10299  canthp1lem2  10576  gchdju1  10579  pwfseqlem3  10583  inttsk  10697  r1tskina  10705  nqereu  10852  zbtwnre  12896  discr1  14201  seqcoll2  14427  bitsfzo  16404  bitsf1  16415  eucalglt  16554  4sqlem17  16932  4sqlem18  16933  ramubcl  16989  psgnunilem5  19469  odnncl  19520  gexnnod  19563  sylow1lem1  19573  torsubg  19829  prmcyg  19869  ablfacrplem  20042  pgpfac1lem2  20052  pgpfac1lem3a  20053  pgpfac1lem3  20054  xrsdsreclblem  21393  prmirredlem  21452  ppttop  22972  pptbas  22973  regr1lem  23704  alexsublem  24009  reconnlem1  24792  metnrmlem1a  24824  vitalilem4  25578  vitalilem5  25579  itg2gt0  25727  rollelem  25956  lhop1lem  25980  coefv0  26213  plyexmo  26279  lgamucov  27001  ppinprm  27115  chtnprm  27117  lgsdir  27295  lgseisenlem1  27338  2sqlem7  27387  2sqblem  27394  pntpbnd1  27549  madebdaylemlrcut  27891  bdayfinbndlem1  28459  dfon2lem8  35970  poimirlem25  37966  fdc  38066  ac6s6  38493  2atm  39973  llnmlplnN  39985  trlval3  40633  cdleme0moN  40671  cdleme18c  40739  qirropth  43336  aacllem  50276