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  8475  nnaordi  8548  fineqvlem  9170  dif1ennnALT  9181  rankr1ag  9720  cfslb2n  10184  fin23lem27  10244  gchpwdom  10587  prlem934  10950  axpre-sup  11086  cju  12149  xrub  13258  facavg  14257  mulcn2  15552  o1rlimmul  15575  coprm  16675  rpexp  16686  vdwnnlem3  16962  gexdvds  19553  cnpnei  23242  comppfsc  23510  alexsubALTlem3  24027  alexsubALTlem4  24028  iccntr  24800  cfil3i  25249  bcth3  25311  lgseisenlem2  27356  cusgredg  29510  uspgr2wlkeq  29732  ubthlem1  30959  staddi  32335  stadd3i  32337  addltmulALT  32535  expgt0b  32908  cnre2csqlem  34073  tpr2rico  34075  satffunlem2lem1  35605  mclsax  35770  dfrdg4  36152  segconeq  36211  nn0prpwlem  36523  bj-bary1lem1  37644  poimirlem29  37987  fdc  38083  bfplem2  38161  atexchcvrN  39903  dalem3  40127  cdleme3h  40698  cdleme21ct  40792  oexpreposd  42771  cantnfresb  43773  omabs2  43781  naddwordnexlem4  43850  sbgoldbwt  48268  sbgoldbst  48269  nnsum4primesodd  48287  nnsum4primesoddALTV  48288  dignn0flhalflem1  49106