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 ⊢ (𝜑 → (𝜓 → 𝜏))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  oaordi  8554  nnaordi  8627  fineqvlem  9257  dif1ennnALT  9268  rankr1ag  9810  cfslb2n  10346  fin23lem27  10406  gchpwdom  10755  prlem934  11118  axpre-sup  11254  cju  12316  xrub  13442  facavg  14445  mulcn2  15763  o1rlimmul  15786  coprm  16887  rpexp  16898  vdwnnlem3  17175  gexdvds  19798  cnpnei  23582  comppfsc  23851  alexsubALTlem3  24368  alexsubALTlem4  24369  iccntr  25141  cfil3i  25590  bcth3  25652  lgseisenlem2  27703  fltoprm  27995  cusgredg  30005  uspgr2wlkeq  30226  ubthlem1  31472  staddi  32848  stadd3i  32850  addltmulALT  33048  expgt0b  33408  cnre2csqlem  34542  tpr2rico  34544  satffunlem2lem1  36169  mclsax  36334  dfrdg4  36715  segconeq  36775  nn0prpwlem  37110  bj-bary1lem1  38232  poimirlem29  38567  findcard4  38632  fdc  38679  bfplem2  38757  atexchcvrN  40497  dalem3  40721  cdleme3h  41292  cdleme21ct  41386  oexpreposd  43379  cantnfresb  44325  omabs2  44333  naddwordnexlem4  44402  sbgoldbwt  48874  sbgoldbst  48875  nnsum4primesodd  48893  nnsum4primesoddALTV  48894  dignn0flhalflem1  49726