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  875  ecase23d  1469  disjss3  5148  nnsuc  7889  poxp2  8148  frrlem14  8305  unxpdomlem2  9276  oismo  9565  cnfcom3lem  9728  rankelb  9849  fin33i  10394  isf34lem4  10402  canthp1lem2  10678  gchdju1  10681  pwfseqlem3  10685  inttsk  10799  r1tskina  10807  nqereu  10954  zbtwnre  12963  discr1  14237  seqcoll2  14462  bitsfzo  16413  bitsf1  16424  eucalglt  16559  4sqlem17  16933  4sqlem18  16934  ramubcl  16990  psgnunilem5  19461  odnncl  19512  gexnnod  19555  sylow1lem1  19565  torsubg  19821  prmcyg  19861  ablfacrplem  20034  pgpfac1lem2  20044  pgpfac1lem3a  20045  pgpfac1lem3  20046  xrsdsreclblem  21362  prmirredlem  21415  ppttop  22954  pptbas  22955  regr1lem  23687  alexsublem  23992  reconnlem1  24786  metnrmlem1a  24818  vitalilem4  25584  vitalilem5  25585  itg2gt0  25734  rollelem  25965  lhop1lem  25990  coefv0  26227  plyexmo  26293  lgamucov  27015  ppinprm  27129  chtnprm  27131  lgsdir  27310  lgseisenlem1  27353  2sqlem7  27402  2sqblem  27409  pntpbnd1  27564  madebdaylemlrcut  27871  dfon2lem8  35517  poimirlem25  37249  fdc  37349  ac6s6  37776  2atm  39130  llnmlplnN  39142  trlval3  39790  cdleme0moN  39828  cdleme18c  39896  qirropth  42470  aacllem  48420