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  8487  nnaordi  8559  fineqvlem  9185  dif1ennnALT  9198  xpfiOLD  9246  rankr1ag  9731  cfslb2n  10197  fin23lem27  10257  gchpwdom  10599  prlem934  10962  axpre-sup  11098  cju  12158  xrub  13248  facavg  14242  mulcn2  15538  o1rlimmul  15561  coprm  16657  rpexp  16668  vdwnnlem3  16944  gexdvds  19498  cnpnei  23184  comppfsc  23452  alexsubALTlem3  23969  alexsubALTlem4  23970  iccntr  24743  cfil3i  25202  bcth3  25264  lgseisenlem2  27320  cusgredg  29404  uspgr2wlkeq  29626  ubthlem1  30849  staddi  32225  stadd3i  32227  addltmulALT  32425  expgt0b  32791  cnre2csqlem  33893  tpr2rico  33895  satffunlem2lem1  35384  mclsax  35549  dfrdg4  35932  segconeq  35991  nn0prpwlem  36303  bj-bary1lem1  37292  poimirlem29  37636  fdc  37732  bfplem2  37810  atexchcvrN  39427  dalem3  39651  cdleme3h  40222  cdleme21ct  40316  oexpreposd  42303  cantnfresb  43306  omabs2  43314  naddwordnexlem4  43383  sbgoldbwt  47771  sbgoldbst  47772  nnsum4primesodd  47790  nnsum4primesoddALTV  47791  dignn0flhalflem1  48597