Theorem mt3d 150

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 147	. 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  151  nsyl2OLD  152  olcnd  873  ecase23d  1469  disjss3  5065  nnsuc  7597  unxpdomlem2  8723  oismo  9004  cnfcom3lem  9166  rankelb  9253  fin33i  9791  isf34lem4  9799  canthp1lem2  10075  gchdju1  10078  pwfseqlem3  10082  inttsk  10196  r1tskina  10204  nqereu  10351  zbtwnre  12347  discr1  13601  seqcoll2  13824  bitsfzo  15784  bitsf1  15795  eucalglt  15929  4sqlem17  16297  4sqlem18  16298  ramubcl  16354  psgnunilem5  18622  odnncl  18673  gexnnod  18713  sylow1lem1  18723  torsubg  18974  prmcyg  19014  ablfacrplem  19187  pgpfac1lem2  19197  pgpfac1lem3a  19198  pgpfac1lem3  19199  xrsdsreclblem  20591  prmirredlem  20640  ppttop  21615  pptbas  21616  regr1lem  22347  alexsublem  22652  reconnlem1  23434  metnrmlem1a  23466  vitalilem4  24212  vitalilem5  24213  itg2gt0  24361  rollelem  24586  lhop1lem  24610  coefv0  24838  plyexmo  24902  lgamucov  25615  ppinprm  25729  chtnprm  25731  lgsdir  25908  lgseisenlem1  25951  2sqlem7  26000  2sqblem  26007  pntpbnd1  26162  dfon2lem8  33035  frrlem14  33136  poimirlem25  34932  fdc  35035  ac6s6  35465  2atm  36678  llnmlplnN  36690  trlval3  37338  cdleme0moN  37376  cdleme18c  37444  qirropth  39525  aacllem  44922