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  8461  nnaordi  8533  fineqvlem  9150  dif1ennnALT  9161  rankr1ag  9695  cfslb2n  10159  fin23lem27  10219  gchpwdom  10561  prlem934  10924  axpre-sup  11060  cju  12121  xrub  13211  facavg  14208  mulcn2  15503  o1rlimmul  15526  coprm  16622  rpexp  16633  vdwnnlem3  16909  gexdvds  19496  cnpnei  23179  comppfsc  23447  alexsubALTlem3  23964  alexsubALTlem4  23965  iccntr  24737  cfil3i  25196  bcth3  25258  lgseisenlem2  27314  cusgredg  29402  uspgr2wlkeq  29624  ubthlem1  30850  staddi  32226  stadd3i  32228  addltmulALT  32426  expgt0b  32799  cnre2csqlem  33923  tpr2rico  33925  satffunlem2lem1  35448  mclsax  35613  dfrdg4  35995  segconeq  36054  nn0prpwlem  36366  bj-bary1lem1  37355  poimirlem29  37699  fdc  37795  bfplem2  37873  atexchcvrN  39549  dalem3  39773  cdleme3h  40344  cdleme21ct  40438  oexpreposd  42425  cantnfresb  43427  omabs2  43435  naddwordnexlem4  43504  sbgoldbwt  47887  sbgoldbst  47888  nnsum4primesodd  47906  nnsum4primesoddALTV  47907  dignn0flhalflem1  48726