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  5094  nnsuc  7824  poxp2  8083  frrlem14  8239  unxpdomlem2  9156  oismo  9451  cnfcom3lem  9618  rankelb  9739  fin33i  10282  isf34lem4  10290  canthp1lem2  10566  gchdju1  10569  pwfseqlem3  10573  inttsk  10687  r1tskina  10695  nqereu  10842  zbtwnre  12865  discr1  14164  seqcoll2  14390  bitsfzo  16364  bitsf1  16375  eucalglt  16514  4sqlem17  16891  4sqlem18  16892  ramubcl  16948  psgnunilem5  19391  odnncl  19442  gexnnod  19485  sylow1lem1  19495  torsubg  19751  prmcyg  19791  ablfacrplem  19964  pgpfac1lem2  19974  pgpfac1lem3a  19975  pgpfac1lem3  19976  xrsdsreclblem  21337  prmirredlem  21397  ppttop  22910  pptbas  22911  regr1lem  23642  alexsublem  23947  reconnlem1  24731  metnrmlem1a  24763  vitalilem4  25528  vitalilem5  25529  itg2gt0  25677  rollelem  25909  lhop1lem  25934  coefv0  26169  plyexmo  26237  lgamucov  26964  ppinprm  27078  chtnprm  27080  lgsdir  27259  lgseisenlem1  27302  2sqlem7  27351  2sqblem  27358  pntpbnd1  27513  madebdaylemlrcut  27831  dfon2lem8  35763  poimirlem25  37624  fdc  37724  ac6s6  38151  2atm  39506  llnmlplnN  39518  trlval3  40166  cdleme0moN  40204  cdleme18c  40272  qirropth  42881  aacllem  49787