Theorem 3syld 61

Description: Triple syllogism deduction. Deduction associated with 3syld 61. (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 48	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
4		3syld.3	. 2 ⊢ (𝜑 → (𝜃 → 𝜏))
5	3, 4	syld 48	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  8527  nnaordi  8600  fineqvlem  9222  dif1ennnALT  9233  rankr1ag  9770  cfslb2n  10247  fin23lem27  10307  gchpwdom  10650  prlem934  11013  axpre-sup  11149  cju  12209  xrub  13333  facavg  14333  mulcn2  15643  o1rlimmul  15666  coprm  16765  rpexp  16776  vdwnnlem3  17052  gexdvds  19649  cnpnei  23421  comppfsc  23689  alexsubALTlem3  24206  alexsubALTlem4  24207  iccntr  24979  cfil3i  25428  bcth3  25490  lgseisenlem2  27540  cusgredg  29774  uspgr2wlkeq  29995  ubthlem1  31222  staddi  32598  stadd3i  32600  addltmulALT  32798  expgt0b  33161  cnre2csqlem  34300  tpr2rico  34302  satffunlem2lem1  35896  mclsax  36061  dfrdg4  36443  segconeq  36502  nn0prpwlem  36853  bj-bary1lem1  37975  poimirlem29  38320  fdc  38416  bfplem2  38494  atexchcvrN  40234  dalem3  40458  cdleme3h  41029  cdleme21ct  41123  oexpreposd  43103  cantnfresb  44071  omabs2  44079  naddwordnexlem4  44148  sbgoldbwt  48562  sbgoldbst  48563  nnsum4primesodd  48581  nnsum4primesoddALTV  48582  dignn0flhalflem1  49415