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  8464  nnaordi  8536  fineqvlem  9155  dif1ennnALT  9166  rankr1ag  9698  cfslb2n  10162  fin23lem27  10222  gchpwdom  10564  prlem934  10927  axpre-sup  11063  cju  12124  xrub  13214  facavg  14208  mulcn2  15503  o1rlimmul  15526  coprm  16622  rpexp  16633  vdwnnlem3  16909  gexdvds  19463  cnpnei  23149  comppfsc  23417  alexsubALTlem3  23934  alexsubALTlem4  23935  iccntr  24708  cfil3i  25167  bcth3  25229  lgseisenlem2  27285  cusgredg  29369  uspgr2wlkeq  29591  ubthlem1  30814  staddi  32190  stadd3i  32192  addltmulALT  32390  expgt0b  32761  cnre2csqlem  33877  tpr2rico  33879  satffunlem2lem1  35381  mclsax  35546  dfrdg4  35929  segconeq  35988  nn0prpwlem  36300  bj-bary1lem1  37289  poimirlem29  37633  fdc  37729  bfplem2  37807  atexchcvrN  39423  dalem3  39647  cdleme3h  40218  cdleme21ct  40312  oexpreposd  42299  cantnfresb  43301  omabs2  43309  naddwordnexlem4  43378  sbgoldbwt  47765  sbgoldbst  47766  nnsum4primesodd  47784  nnsum4primesoddALTV  47785  dignn0flhalflem1  48604