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  873  ecase23d  1471  disjss3  5069  nnsuc  7705  frrlem14  8086  unxpdomlem2  8957  oismo  9229  cnfcom3lem  9391  rankelb  9513  fin33i  10056  isf34lem4  10064  canthp1lem2  10340  gchdju1  10343  pwfseqlem3  10347  inttsk  10461  r1tskina  10469  nqereu  10616  zbtwnre  12615  discr1  13882  seqcoll2  14107  bitsfzo  16070  bitsf1  16081  eucalglt  16218  4sqlem17  16590  4sqlem18  16591  ramubcl  16647  psgnunilem5  19017  odnncl  19068  gexnnod  19108  sylow1lem1  19118  torsubg  19370  prmcyg  19410  ablfacrplem  19583  pgpfac1lem2  19593  pgpfac1lem3a  19594  pgpfac1lem3  19595  xrsdsreclblem  20556  prmirredlem  20606  ppttop  22065  pptbas  22066  regr1lem  22798  alexsublem  23103  reconnlem1  23895  metnrmlem1a  23927  vitalilem4  24680  vitalilem5  24681  itg2gt0  24830  rollelem  25058  lhop1lem  25082  coefv0  25314  plyexmo  25378  lgamucov  26092  ppinprm  26206  chtnprm  26208  lgsdir  26385  lgseisenlem1  26428  2sqlem7  26477  2sqblem  26484  pntpbnd1  26639  dfon2lem8  33672  poxp2  33717  poxp3  33723  madebdaylemlrcut  34006  poimirlem25  35729  fdc  35830  ac6s6  36257  2atm  37468  llnmlplnN  37480  trlval3  38128  cdleme0moN  38166  cdleme18c  38234  qirropth  40646  aacllem  46391