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  8165  nnaordi  8237  fineqvlem  8725  dif1en  8744  xpfi  8782  rankr1ag  9224  cfslb2n  9683  fin23lem27  9743  gchpwdom  10085  prlem934  10448  axpre-sup  10584  cju  11627  xrub  12699  facavg  13658  mulcn2  14947  o1rlimmul  14970  coprm  16050  rpexp  16059  vdwnnlem3  16328  gexdvds  18704  cnpnei  21867  comppfsc  22135  alexsubALTlem3  22652  alexsubALTlem4  22653  iccntr  23424  cfil3i  23867  bcth3  23929  lgseisenlem2  25950  cusgredg  27204  uspgr2wlkeq  27425  ubthlem1  28645  staddi  30021  stadd3i  30023  addltmulALT  30221  cnre2csqlem  31174  tpr2rico  31176  satffunlem2lem1  32672  mclsax  32837  dfrdg4  33433  segconeq  33492  nn0prpwlem  33691  bj-bary1lem1  34616  poimirlem29  34956  fdc  35053  bfplem2  35134  atexchcvrN  36609  dalem3  36833  cdleme3h  37404  cdleme21ct  37498  oexpreposd  39255  sbgoldbwt  44016  sbgoldbst  44017  nnsum4primesodd  44035  nnsum4primesoddALTV  44036  dignn0flhalflem1  44749