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  8602  nnaordi  8674  fineqvlem  9325  dif1ennnALT  9339  xpfiOLD  9387  rankr1ag  9871  cfslb2n  10337  fin23lem27  10397  gchpwdom  10739  prlem934  11102  axpre-sup  11238  cju  12289  xrub  13374  facavg  14350  mulcn2  15642  o1rlimmul  15665  coprm  16758  rpexp  16769  vdwnnlem3  17044  gexdvds  19626  cnpnei  23293  comppfsc  23561  alexsubALTlem3  24078  alexsubALTlem4  24079  iccntr  24862  cfil3i  25322  bcth3  25384  lgseisenlem2  27438  cusgredg  29459  uspgr2wlkeq  29682  ubthlem1  30902  staddi  32278  stadd3i  32280  addltmulALT  32478  expgt0b  32820  cnre2csqlem  33856  tpr2rico  33858  satffunlem2lem1  35372  mclsax  35537  dfrdg4  35915  segconeq  35974  nn0prpwlem  36288  bj-bary1lem1  37277  poimirlem29  37609  fdc  37705  bfplem2  37783  atexchcvrN  39397  dalem3  39621  cdleme3h  40192  cdleme21ct  40286  oexpreposd  42309  cantnfresb  43286  omabs2  43294  naddwordnexlem4  43363  sbgoldbwt  47651  sbgoldbst  47652  nnsum4primesodd  47670  nnsum4primesoddALTV  47671  dignn0flhalflem1  48349