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  877  disjss3  5092  nnsuc  7820  poxp2  8079  frrlem14  8235  unxpdomlem2  9148  oismo  9433  cnfcom3lem  9600  rankelb  9724  fin33i  10267  isf34lem4  10275  canthp1lem2  10551  gchdju1  10554  pwfseqlem3  10558  inttsk  10672  r1tskina  10680  nqereu  10827  zbtwnre  12846  discr1  14148  seqcoll2  14374  bitsfzo  16348  bitsf1  16359  eucalglt  16498  4sqlem17  16875  4sqlem18  16876  ramubcl  16932  psgnunilem5  19408  odnncl  19459  gexnnod  19502  sylow1lem1  19512  torsubg  19768  prmcyg  19808  ablfacrplem  19981  pgpfac1lem2  19991  pgpfac1lem3a  19992  pgpfac1lem3  19993  xrsdsreclblem  21351  prmirredlem  21411  ppttop  22923  pptbas  22924  regr1lem  23655  alexsublem  23960  reconnlem1  24743  metnrmlem1a  24775  vitalilem4  25540  vitalilem5  25541  itg2gt0  25689  rollelem  25921  lhop1lem  25946  coefv0  26181  plyexmo  26249  lgamucov  26976  ppinprm  27090  chtnprm  27092  lgsdir  27271  lgseisenlem1  27314  2sqlem7  27363  2sqblem  27370  pntpbnd1  27525  madebdaylemlrcut  27845  dfon2lem8  35853  poimirlem25  37705  fdc  37805  ac6s6  38232  2atm  39646  llnmlplnN  39658  trlval3  40306  cdleme0moN  40344  cdleme18c  40412  qirropth  43025  aacllem  49926