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  8483  nnaordi  8556  fineqvlem  9178  dif1ennnALT  9189  rankr1ag  9726  cfslb2n  10190  fin23lem27  10250  gchpwdom  10593  prlem934  10956  axpre-sup  11092  cju  12153  xrub  13239  facavg  14236  mulcn2  15531  o1rlimmul  15554  coprm  16650  rpexp  16661  vdwnnlem3  16937  gexdvds  19528  cnpnei  23223  comppfsc  23491  alexsubALTlem3  24008  alexsubALTlem4  24009  iccntr  24781  cfil3i  25240  bcth3  25302  lgseisenlem2  27358  cusgredg  29513  uspgr2wlkeq  29735  ubthlem1  30962  staddi  32338  stadd3i  32340  addltmulALT  32538  expgt0b  32912  cnre2csqlem  34092  tpr2rico  34094  satffunlem2lem1  35624  mclsax  35789  dfrdg4  36171  segconeq  36230  nn0prpwlem  36542  bj-bary1lem1  37570  poimirlem29  37904  fdc  38000  bfplem2  38078  atexchcvrN  39820  dalem3  40044  cdleme3h  40615  cdleme21ct  40709  oexpreposd  42696  cantnfresb  43685  omabs2  43693  naddwordnexlem4  43762  sbgoldbwt  48141  sbgoldbst  48142  nnsum4primesodd  48160  nnsum4primesoddALTV  48161  dignn0flhalflem1  48979