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  8513  nnaordi  8585  fineqvlem  9216  dif1ennnALT  9229  xpfiOLD  9277  rankr1ag  9762  cfslb2n  10228  fin23lem27  10288  gchpwdom  10630  prlem934  10993  axpre-sup  11129  cju  12189  xrub  13279  facavg  14273  mulcn2  15569  o1rlimmul  15592  coprm  16688  rpexp  16699  vdwnnlem3  16975  gexdvds  19521  cnpnei  23158  comppfsc  23426  alexsubALTlem3  23943  alexsubALTlem4  23944  iccntr  24717  cfil3i  25176  bcth3  25238  lgseisenlem2  27294  cusgredg  29358  uspgr2wlkeq  29581  ubthlem1  30806  staddi  32182  stadd3i  32184  addltmulALT  32382  expgt0b  32748  cnre2csqlem  33907  tpr2rico  33909  satffunlem2lem1  35398  mclsax  35563  dfrdg4  35946  segconeq  36005  nn0prpwlem  36317  bj-bary1lem1  37306  poimirlem29  37650  fdc  37746  bfplem2  37824  atexchcvrN  39441  dalem3  39665  cdleme3h  40236  cdleme21ct  40330  oexpreposd  42317  cantnfresb  43320  omabs2  43328  naddwordnexlem4  43397  sbgoldbwt  47782  sbgoldbst  47783  nnsum4primesodd  47801  nnsum4primesoddALTV  47802  dignn0flhalflem1  48608