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  8516  nnaordi  8589  fineqvlem  9211  dif1ennnALT  9222  rankr1ag  9761  cfslb2n  10226  fin23lem27  10286  gchpwdom  10629  prlem934  10992  axpre-sup  11128  cju  12192  xrub  13316  facavg  14315  mulcn2  15624  o1rlimmul  15647  coprm  16747  rpexp  16758  vdwnnlem3  17034  gexdvds  19625  cnpnei  23325  comppfsc  23593  alexsubALTlem3  24110  alexsubALTlem4  24111  iccntr  24883  cfil3i  25332  bcth3  25394  lgseisenlem2  27441  cusgredg  29626  uspgr2wlkeq  29847  ubthlem1  31074  staddi  32450  stadd3i  32452  addltmulALT  32650  expgt0b  33020  cnre2csqlem  34208  tpr2rico  34210  satffunlem2lem1  35755  mclsax  35920  dfrdg4  36302  segconeq  36361  nn0prpwlem  36683  bj-bary1lem1  37804  poimirlem29  38149  fdc  38245  bfplem2  38323  atexchcvrN  40065  dalem3  40289  cdleme3h  40860  cdleme21ct  40954  oexpreposd  42932  cantnfresb  43902  omabs2  43910  naddwordnexlem4  43979  sbgoldbwt  48400  sbgoldbst  48401  nnsum4primesodd  48419  nnsum4primesoddALTV  48420  dignn0flhalflem1  49238