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  8252  nnaordi  8324  fineqvlem  8868  dif1enOLD  8885  xpfi  8920  rankr1ag  9383  cfslb2n  9847  fin23lem27  9907  gchpwdom  10249  prlem934  10612  axpre-sup  10748  cju  11791  xrub  12867  facavg  13832  mulcn2  15122  o1rlimmul  15145  coprm  16231  rpexp  16242  vdwnnlem3  16513  gexdvds  18927  cnpnei  22115  comppfsc  22383  alexsubALTlem3  22900  alexsubALTlem4  22901  iccntr  23672  cfil3i  24120  bcth3  24182  lgseisenlem2  26211  cusgredg  27466  uspgr2wlkeq  27687  ubthlem1  28905  staddi  30281  stadd3i  30283  addltmulALT  30481  cnre2csqlem  31528  tpr2rico  31530  satffunlem2lem1  33033  mclsax  33198  dfrdg4  33939  segconeq  33998  nn0prpwlem  34197  bj-bary1lem1  35165  poimirlem29  35492  fdc  35589  bfplem2  35667  atexchcvrN  37140  dalem3  37364  cdleme3h  37935  cdleme21ct  38029  oexpreposd  39969  sbgoldbwt  44845  sbgoldbst  44846  nnsum4primesodd  44864  nnsum4primesoddALTV  44865  dignn0flhalflem1  45577