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  5099  nnsuc  7836  poxp2  8095  frrlem14  8251  unxpdomlem2  9169  oismo  9457  cnfcom3lem  9624  rankelb  9748  fin33i  10291  isf34lem4  10299  canthp1lem2  10576  gchdju1  10579  pwfseqlem3  10583  inttsk  10697  r1tskina  10705  nqereu  10852  zbtwnre  12871  discr1  14174  seqcoll2  14400  bitsfzo  16374  bitsf1  16385  eucalglt  16524  4sqlem17  16901  4sqlem18  16902  ramubcl  16958  psgnunilem5  19435  odnncl  19486  gexnnod  19529  sylow1lem1  19539  torsubg  19795  prmcyg  19835  ablfacrplem  20008  pgpfac1lem2  20018  pgpfac1lem3a  20019  pgpfac1lem3  20020  xrsdsreclblem  21379  prmirredlem  21439  ppttop  22963  pptbas  22964  regr1lem  23695  alexsublem  24000  reconnlem1  24783  metnrmlem1a  24815  vitalilem4  25580  vitalilem5  25581  itg2gt0  25729  rollelem  25961  lhop1lem  25986  coefv0  26221  plyexmo  26289  lgamucov  27016  ppinprm  27130  chtnprm  27132  lgsdir  27311  lgseisenlem1  27354  2sqlem7  27403  2sqblem  27410  pntpbnd1  27565  madebdaylemlrcut  27907  bdayfinbndlem1  28475  dfon2lem8  36001  poimirlem25  37890  fdc  37990  ac6s6  38417  2atm  39897  llnmlplnN  39909  trlval3  40557  cdleme0moN  40595  cdleme18c  40663  qirropth  43259  aacllem  50154