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  7975  nnaordi  8047  fineqvlem  8529  dif1en  8548  xpfi  8586  rankr1ag  9027  cfslb2n  9490  fin23lem27  9550  gchpwdom  9892  prlem934  10255  axpre-sup  10391  cju  11437  xrub  12524  facavg  13479  mulcn2  14816  o1rlimmul  14839  coprm  15914  rpexp  15923  vdwnnlem3  16192  gexdvds  18473  cnpnei  21579  comppfsc  21847  alexsubALTlem3  22364  alexsubALTlem4  22365  iccntr  23135  cfil3i  23578  bcth3  23640  lgseisenlem2  25657  cusgredg  26912  uspgr2wlkeq  27133  ubthlem1  28428  staddi  29807  stadd3i  29809  addltmulALT  30007  cnre2csqlem  30797  tpr2rico  30799  mclsax  32336  dfrdg4  32933  segconeq  32992  nn0prpwlem  33191  bj-bary1lem1  34040  poimirlem29  34362  fdc  34462  bfplem2  34543  atexchcvrN  36021  dalem3  36245  cdleme3h  36816  cdleme21ct  36910  oexpreposd  38611  sbgoldbwt  43311  sbgoldbst  43312  nnsum4primesodd  43330  nnsum4primesoddALTV  43331  dignn0flhalflem1  44044