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  8510  nnaordi  8582  fineqvlem  9209  dif1ennnALT  9222  xpfiOLD  9270  rankr1ag  9755  cfslb2n  10221  fin23lem27  10281  gchpwdom  10623  prlem934  10986  axpre-sup  11122  cju  12182  xrub  13272  facavg  14266  mulcn2  15562  o1rlimmul  15585  coprm  16681  rpexp  16692  vdwnnlem3  16968  gexdvds  19514  cnpnei  23151  comppfsc  23419  alexsubALTlem3  23936  alexsubALTlem4  23937  iccntr  24710  cfil3i  25169  bcth3  25231  lgseisenlem2  27287  cusgredg  29351  uspgr2wlkeq  29574  ubthlem1  30799  staddi  32175  stadd3i  32177  addltmulALT  32375  expgt0b  32741  cnre2csqlem  33900  tpr2rico  33902  satffunlem2lem1  35391  mclsax  35556  dfrdg4  35939  segconeq  35998  nn0prpwlem  36310  bj-bary1lem1  37299  poimirlem29  37643  fdc  37739  bfplem2  37817  atexchcvrN  39434  dalem3  39658  cdleme3h  40229  cdleme21ct  40323  oexpreposd  42310  cantnfresb  43313  omabs2  43321  naddwordnexlem4  43390  sbgoldbwt  47778  sbgoldbst  47779  nnsum4primesodd  47797  nnsum4primesoddALTV  47798  dignn0flhalflem1  48604