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  8584  nnaordi  8656  fineqvlem  9298  dif1ennnALT  9311  xpfiOLD  9359  rankr1ag  9842  cfslb2n  10308  fin23lem27  10368  gchpwdom  10710  prlem934  11073  axpre-sup  11209  cju  12262  xrub  13354  facavg  14340  mulcn2  15632  o1rlimmul  15655  coprm  16748  rpexp  16759  vdwnnlem3  17035  gexdvds  19602  cnpnei  23272  comppfsc  23540  alexsubALTlem3  24057  alexsubALTlem4  24058  iccntr  24843  cfil3i  25303  bcth3  25365  lgseisenlem2  27420  cusgredg  29441  uspgr2wlkeq  29664  ubthlem1  30889  staddi  32265  stadd3i  32267  addltmulALT  32465  expgt0b  32818  cnre2csqlem  33909  tpr2rico  33911  satffunlem2lem1  35409  mclsax  35574  dfrdg4  35952  segconeq  36011  nn0prpwlem  36323  bj-bary1lem1  37312  poimirlem29  37656  fdc  37752  bfplem2  37830  atexchcvrN  39442  dalem3  39666  cdleme3h  40237  cdleme21ct  40331  oexpreposd  42357  cantnfresb  43337  omabs2  43345  naddwordnexlem4  43414  sbgoldbwt  47764  sbgoldbst  47765  nnsum4primesodd  47783  nnsum4primesoddALTV  47784  dignn0flhalflem1  48536