Theorem 3syld 60

Description: Triple syllogism deduction. Deduction associated with 3syld 60. (Contributed by Jeff Hankins, 4-Aug-2009.)

Hypotheses

Ref	Expression
3syld.1	⊢ (𝜑 → (𝜓 → 𝜒))
3syld.2	⊢ (𝜑 → (𝜒 → 𝜃))
3syld.3	⊢ (𝜑 → (𝜃 → 𝜏))

Assertion

Ref	Expression
3syld	⊢ (𝜑 → (𝜓 → 𝜏))

Proof of Theorem 3syld

Step	Hyp	Ref	Expression
1		3syld.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
2		3syld.2	. . 3 ⊢ (𝜑 → (𝜒 → 𝜃))
3	1, 2	syld 47	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
4		3syld.3	. 2 ⊢ (𝜑 → (𝜃 → 𝜏))
5	3, 4	syld 47	1 ⊢ (𝜑 → (𝜓 → 𝜏))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is referenced by:  oaordi  8471  nnaordi  8544  fineqvlem  9164  dif1ennnALT  9175  rankr1ag  9712  cfslb2n  10176  fin23lem27  10236  gchpwdom  10579  prlem934  10942  axpre-sup  11078  cju  12139  xrub  13225  facavg  14222  mulcn2  15517  o1rlimmul  15540  coprm  16636  rpexp  16647  vdwnnlem3  16923  gexdvds  19511  cnpnei  23206  comppfsc  23474  alexsubALTlem3  23991  alexsubALTlem4  23992  iccntr  24764  cfil3i  25223  bcth3  25285  lgseisenlem2  27341  cusgredg  29446  uspgr2wlkeq  29668  ubthlem1  30894  staddi  32270  stadd3i  32272  addltmulALT  32470  expgt0b  32846  cnre2csqlem  34016  tpr2rico  34018  satffunlem2lem1  35547  mclsax  35712  dfrdg4  36094  segconeq  36153  nn0prpwlem  36465  bj-bary1lem1  37455  poimirlem29  37789  fdc  37885  bfplem2  37963  atexchcvrN  39639  dalem3  39863  cdleme3h  40434  cdleme21ct  40528  oexpreposd  42519  cantnfresb  43508  omabs2  43516  naddwordnexlem4  43585  sbgoldbwt  47965  sbgoldbst  47966  nnsum4primesodd  47984  nnsum4primesoddALTV  47985  dignn0flhalflem1  48803