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  8481  nnaordi  8554  fineqvlem  9176  dif1ennnALT  9187  rankr1ag  9726  cfslb2n  10190  fin23lem27  10250  gchpwdom  10593  prlem934  10956  axpre-sup  11092  cju  12155  xrub  13264  facavg  14263  mulcn2  15558  o1rlimmul  15581  coprm  16681  rpexp  16692  vdwnnlem3  16968  gexdvds  19559  cnpnei  23229  comppfsc  23497  alexsubALTlem3  24014  alexsubALTlem4  24015  iccntr  24787  cfil3i  25236  bcth3  25298  lgseisenlem2  27339  cusgredg  29493  uspgr2wlkeq  29714  ubthlem1  30941  staddi  32317  stadd3i  32319  addltmulALT  32517  expgt0b  32890  cnre2csqlem  34054  tpr2rico  34056  satffunlem2lem1  35586  mclsax  35751  dfrdg4  36133  segconeq  36192  nn0prpwlem  36504  bj-bary1lem1  37625  poimirlem29  37970  fdc  38066  bfplem2  38144  atexchcvrN  39886  dalem3  40110  cdleme3h  40681  cdleme21ct  40775  oexpreposd  42754  cantnfresb  43752  omabs2  43760  naddwordnexlem4  43829  sbgoldbwt  48253  sbgoldbst  48254  nnsum4primesodd  48272  nnsum4primesoddALTV  48273  dignn0flhalflem1  49091