Theorem mt3d 149

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 146	. 2 ⊢ (𝜑 → (¬ 𝜒 → 𝜓))
4	1, 3	mpd 16	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  150  olcnd  890  disjss3  5109  nnsuc  7881  poxp2  8140  frrlem14  8297  unxpdomlem2  9218  oismo  9503  cnfcom3lem  9673  rankelb  9797  fin33i  10354  isf34lem4  10362  canthp1lem2  10639  gchdju1  10642  pwfseqlem3  10646  inttsk  10760  r1tskina  10768  nqereu  10915  zbtwnre  12971  discr1  14277  seqcoll2  14504  bitsfzo  16494  bitsf1  16505  eucalglt  16644  4sqlem17  17022  4sqlem18  17023  ramubcl  17079  psgnunilem5  19565  odnncl  19616  gexnnod  19659  sylow1lem1  19669  torsubg  19925  prmcyg  19965  ablfacrplem  20138  pgpfac1lem2  20148  pgpfac1lem3a  20149  pgpfac1lem3  20150  xrsdsreclblem  21544  prmirredlem  21603  ppttop  23145  pptbas  23146  regr1lem  23877  alexsublem  24182  reconnlem1  24965  metnrmlem1a  24997  vitalilem4  25751  vitalilem5  25752  itg2gt0  25900  rollelem  26129  lhop1lem  26153  coefv0  26386  plyexmo  26455  lgamucov  27180  ppinprm  27294  chtnprm  27296  lgsdir  27474  lgseisenlem1  27517  2sqlem7  27566  2sqblem  27573  pntpbnd1  27728  madebdaylemlrcut  28070  bdayfinbndlem1  28638  dfon2lem8  36258  poimirlem25  38274  fdc  38374  ac6s6  38799  2atm  40279  llnmlplnN  40291  trlval3  40939  cdleme0moN  40977  cdleme18c  41045  qirropth  43615  aacllem  50578