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  877  disjss3  5123  nnsuc  7884  poxp2  8147  frrlem14  8303  unxpdomlem2  9264  oismo  9559  cnfcom3lem  9722  rankelb  9843  fin33i  10388  isf34lem4  10396  canthp1lem2  10672  gchdju1  10675  pwfseqlem3  10679  inttsk  10793  r1tskina  10801  nqereu  10948  zbtwnre  12967  discr1  14262  seqcoll2  14488  bitsfzo  16459  bitsf1  16470  eucalglt  16609  4sqlem17  16986  4sqlem18  16987  ramubcl  17043  psgnunilem5  19480  odnncl  19531  gexnnod  19574  sylow1lem1  19584  torsubg  19840  prmcyg  19880  ablfacrplem  20053  pgpfac1lem2  20063  pgpfac1lem3a  20064  pgpfac1lem3  20065  xrsdsreclblem  21385  prmirredlem  21438  ppttop  22950  pptbas  22951  regr1lem  23682  alexsublem  23987  reconnlem1  24771  metnrmlem1a  24803  vitalilem4  25569  vitalilem5  25570  itg2gt0  25718  rollelem  25950  lhop1lem  25975  coefv0  26210  plyexmo  26278  lgamucov  27005  ppinprm  27119  chtnprm  27121  lgsdir  27300  lgseisenlem1  27343  2sqlem7  27392  2sqblem  27399  pntpbnd1  27554  madebdaylemlrcut  27867  dfon2lem8  35813  poimirlem25  37674  fdc  37774  ac6s6  38201  2atm  39551  llnmlplnN  39563  trlval3  40211  cdleme0moN  40249  cdleme18c  40317  qirropth  42898  aacllem  49632