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  8464  nnaordi  8536  fineqvlem  9155  dif1ennnALT  9166  rankr1ag  9698  cfslb2n  10162  fin23lem27  10222  gchpwdom  10564  prlem934  10927  axpre-sup  11063  cju  12124  xrub  13214  facavg  14208  mulcn2  15503  o1rlimmul  15526  coprm  16622  rpexp  16633  vdwnnlem3  16909  gexdvds  19463  cnpnei  23149  comppfsc  23417  alexsubALTlem3  23934  alexsubALTlem4  23935  iccntr  24708  cfil3i  25167  bcth3  25229  lgseisenlem2  27285  cusgredg  29369  uspgr2wlkeq  29591  ubthlem1  30814  staddi  32190  stadd3i  32192  addltmulALT  32390  expgt0b  32762  cnre2csqlem  33883  tpr2rico  33885  satffunlem2lem1  35387  mclsax  35552  dfrdg4  35935  segconeq  35994  nn0prpwlem  36306  bj-bary1lem1  37295  poimirlem29  37639  fdc  37735  bfplem2  37813  atexchcvrN  39429  dalem3  39653  cdleme3h  40224  cdleme21ct  40318  oexpreposd  42305  cantnfresb  43307  omabs2  43315  naddwordnexlem4  43384  sbgoldbwt  47771  sbgoldbst  47772  nnsum4primesodd  47790  nnsum4primesoddALTV  47791  dignn0flhalflem1  48610