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  8531  nnaordi  8604  fineqvlem  9226  dif1ennnALT  9237  rankr1ag  9774  cfslb2n  10252  fin23lem27  10312  gchpwdom  10655  prlem934  11018  axpre-sup  11154  cju  12214  xrub  13338  facavg  14337  mulcn2  15647  o1rlimmul  15670  coprm  16770  rpexp  16781  vdwnnlem3  17057  gexdvds  19654  cnpnei  23390  comppfsc  23658  alexsubALTlem3  24175  alexsubALTlem4  24176  iccntr  24948  cfil3i  25397  bcth3  25459  lgseisenlem2  27506  cusgredg  29715  uspgr2wlkeq  29936  ubthlem1  31163  staddi  32539  stadd3i  32541  addltmulALT  32739  expgt0b  33102  cnre2csqlem  34245  tpr2rico  34247  satffunlem2lem1  35829  mclsax  35994  dfrdg4  36376  segconeq  36435  nn0prpwlem  36756  bj-bary1lem1  37877  poimirlem29  38222  fdc  38318  bfplem2  38396  atexchcvrN  40138  dalem3  40362  cdleme3h  40933  cdleme21ct  41027  oexpreposd  43007  cantnfresb  43977  omabs2  43985  naddwordnexlem4  44054  sbgoldbwt  48465  sbgoldbst  48466  nnsum4primesodd  48484  nnsum4primesoddALTV  48485  dignn0flhalflem1  49314