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  8519  nnaordi  8592  fineqvlem  9214  dif1ennnALT  9225  rankr1ag  9762  cfslb2n  10240  fin23lem27  10300  gchpwdom  10643  prlem934  11006  axpre-sup  11142  cju  12205  xrub  13329  facavg  14328  mulcn2  15637  o1rlimmul  15660  coprm  16760  rpexp  16771  vdwnnlem3  17047  gexdvds  19645  cnpnei  23382  comppfsc  23650  alexsubALTlem3  24167  alexsubALTlem4  24168  iccntr  24940  cfil3i  25389  bcth3  25451  lgseisenlem2  27498  cusgredg  29683  uspgr2wlkeq  29904  ubthlem1  31131  staddi  32507  stadd3i  32509  addltmulALT  32707  expgt0b  33074  cnre2csqlem  34217  tpr2rico  34219  satffunlem2lem1  35767  mclsax  35932  dfrdg4  36314  segconeq  36373  nn0prpwlem  36695  bj-bary1lem1  37815  poimirlem29  38160  fdc  38256  bfplem2  38334  atexchcvrN  40076  dalem3  40300  cdleme3h  40871  cdleme21ct  40965  oexpreposd  42943  cantnfresb  43913  omabs2  43921  naddwordnexlem4  43990  sbgoldbwt  48397  sbgoldbst  48398  nnsum4primesodd  48416  nnsum4primesoddALTV  48417  dignn0flhalflem1  49246