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  7798  nnaordi  7870  fineqvlem  8342  dif1en  8361  xpfi  8399  rankr1ag  8841  cfslb2n  9303  fin23lem27  9363  gchpwdom  9705  prlem934  10068  axpre-sup  10203  cju  11229  xrub  12356  facavg  13303  mulcn2  14546  o1rlimmul  14569  coprm  15646  rpexp  15655  vdwnnlem3  15924  gexdvds  18220  cnpnei  21291  comppfsc  21558  alexsubALTlem3  22075  alexsubALTlem4  22076  iccntr  22846  cfil3i  23288  bcth3  23349  lgseisenlem2  25322  cusgredg  26552  uspgr2wlkeq  26774  ubthlem1  28057  staddi  29436  stadd3i  29438  addltmulALT  29636  cnre2csqlem  30287  tpr2rico  30289  mclsax  31795  dfrdg4  32386  segconeq  32445  nn0prpwlem  32645  bj-bary1lem1  33491  poimirlem29  33770  fdc  33873  bfplem2  33954  atexchcvrN  35248  dalem3  35472  cdleme3h  36044  cdleme21ct  36138  sbgoldbwt  42194  sbgoldbst  42195  nnsum4primesodd  42213  nnsum4primesoddALTV  42214  dignn0flhalflem1  42938