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  8377  nnaordi  8449  fineqvlem  9037  dif1enALT  9050  xpfi  9085  rankr1ag  9560  cfslb2n  10024  fin23lem27  10084  gchpwdom  10426  prlem934  10789  axpre-sup  10925  cju  11969  xrub  13046  facavg  14015  mulcn2  15305  o1rlimmul  15328  coprm  16416  rpexp  16427  vdwnnlem3  16698  gexdvds  19189  cnpnei  22415  comppfsc  22683  alexsubALTlem3  23200  alexsubALTlem4  23201  iccntr  23984  cfil3i  24433  bcth3  24495  lgseisenlem2  26524  cusgredg  27791  uspgr2wlkeq  28013  ubthlem1  29232  staddi  30608  stadd3i  30610  addltmulALT  30808  cnre2csqlem  31860  tpr2rico  31862  satffunlem2lem1  33366  mclsax  33531  dfrdg4  34253  segconeq  34312  nn0prpwlem  34511  bj-bary1lem1  35482  poimirlem29  35806  fdc  35903  bfplem2  35981  atexchcvrN  37454  dalem3  37678  cdleme3h  38249  cdleme21ct  38343  oexpreposd  40321  sbgoldbwt  45229  sbgoldbst  45230  nnsum4primesodd  45248  nnsum4primesoddALTV  45249  dignn0flhalflem1  45961