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  883  disjss3  5078  nnsuc  7831  poxp2  8090  frrlem14  8246  unxpdomlem2  9164  oismo  9452  cnfcom3lem  9622  rankelb  9746  fin33i  10289  isf34lem4  10297  canthp1lem2  10574  gchdju1  10577  pwfseqlem3  10581  inttsk  10695  r1tskina  10703  nqereu  10850  zbtwnre  12894  discr1  14199  seqcoll2  14425  bitsfzo  16402  bitsf1  16413  eucalglt  16552  4sqlem17  16930  4sqlem18  16931  ramubcl  16987  psgnunilem5  19467  odnncl  19518  gexnnod  19561  sylow1lem1  19571  torsubg  19827  prmcyg  19867  ablfacrplem  20040  pgpfac1lem2  20050  pgpfac1lem3a  20051  pgpfac1lem3  20052  xrsdsreclblem  21395  prmirredlem  21454  ppttop  22997  pptbas  22998  regr1lem  23729  alexsublem  24034  reconnlem1  24817  metnrmlem1a  24849  vitalilem4  25603  vitalilem5  25604  itg2gt0  25752  rollelem  25981  lhop1lem  26005  coefv0  26238  plyexmo  26304  lgamucov  27026  ppinprm  27140  chtnprm  27142  lgsdir  27320  lgseisenlem1  27363  2sqlem7  27412  2sqblem  27419  pntpbnd1  27574  madebdaylemlrcut  27916  bdayfinbndlem1  28484  dfon2lem8  36023  poimirlem25  38019  fdc  38119  ac6s6  38546  2atm  40026  llnmlplnN  40038  trlval3  40686  cdleme0moN  40724  cdleme18c  40792  qirropth  43360  aacllem  50298