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  5109  nnsuc  7863  poxp2  8125  frrlem14  8281  unxpdomlem2  9205  oismo  9500  cnfcom3lem  9663  rankelb  9784  fin33i  10329  isf34lem4  10337  canthp1lem2  10613  gchdju1  10616  pwfseqlem3  10620  inttsk  10734  r1tskina  10742  nqereu  10889  zbtwnre  12912  discr1  14211  seqcoll2  14437  bitsfzo  16412  bitsf1  16423  eucalglt  16562  4sqlem17  16939  4sqlem18  16940  ramubcl  16996  psgnunilem5  19431  odnncl  19482  gexnnod  19525  sylow1lem1  19535  torsubg  19791  prmcyg  19831  ablfacrplem  20004  pgpfac1lem2  20014  pgpfac1lem3a  20015  pgpfac1lem3  20016  xrsdsreclblem  21336  prmirredlem  21389  ppttop  22901  pptbas  22902  regr1lem  23633  alexsublem  23938  reconnlem1  24722  metnrmlem1a  24754  vitalilem4  25519  vitalilem5  25520  itg2gt0  25668  rollelem  25900  lhop1lem  25925  coefv0  26160  plyexmo  26228  lgamucov  26955  ppinprm  27069  chtnprm  27071  lgsdir  27250  lgseisenlem1  27293  2sqlem7  27342  2sqblem  27349  pntpbnd1  27504  madebdaylemlrcut  27817  dfon2lem8  35785  poimirlem25  37646  fdc  37746  ac6s6  38173  2atm  39528  llnmlplnN  39540  trlval3  40188  cdleme0moN  40226  cdleme18c  40294  qirropth  42903  aacllem  49794