Theorem 3syld 58

Description: Triple syllogism deduction. Deduction associated with 3syld 58. (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 46	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
4		3syld.3	. 2 ⊢ (𝜑 → (𝜃 → 𝜏))
5	3, 4	syld 46	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  7513  nnaordi  7585  fineqvlem  8059  dif1en  8078  xpfi  8116  rankr1ag  8548  cfslb2n  8973  fin23lem27  9033  gchpwdom  9371  prlem934  9734  axpre-sup  9869  cju  10893  xrub  12014  facavg  12950  mulcn2  14174  o1rlimmul  14197  coprm  15261  rpexp  15270  vdwnnlem3  15539  gexdvds  17822  cnpnei  20878  comppfsc  21145  alexsubALTlem3  21663  alexsubALTlem4  21664  iccntr  22432  cfil3i  22875  bcth3  22936  lgseisenlem2  24901  usgrasscusgra  26011  usg2wlkeq  26236  nbhashuvtx1  26442  frgrawopreglem4  26574  ubthlem1  27110  staddi  28489  stadd3i  28491  addltmulALT  28689  cnre2csqlem  29284  tpr2rico  29286  mclsax  30720  dfrdg4  31228  segconeq  31287  nn0prpwlem  31487  bj-bary1lem1  32338  poimirlem29  32608  fdc  32711  bfplem2  32792  atexchcvrN  33744  dalem3  33968  cdleme3h  34540  cdleme21ct  34635  bgoldbwt  40199  bgoldbst  40200  nnsum4primesodd  40212  nnsum4primesoddALTV  40213  cusgredg  40646  uspgr2wlkeq  40854  frgrwopreglem4  41484  dignn0flhalflem1  42207