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  8473  nnaordi  8546  fineqvlem  9168  dif1ennnALT  9179  rankr1ag  9716  cfslb2n  10180  fin23lem27  10240  gchpwdom  10583  prlem934  10946  axpre-sup  11082  cju  12143  xrub  13229  facavg  14226  mulcn2  15521  o1rlimmul  15544  coprm  16640  rpexp  16651  vdwnnlem3  16927  gexdvds  19515  cnpnei  23210  comppfsc  23478  alexsubALTlem3  23995  alexsubALTlem4  23996  iccntr  24768  cfil3i  25227  bcth3  25289  lgseisenlem2  27345  cusgredg  29499  uspgr2wlkeq  29721  ubthlem1  30947  staddi  32323  stadd3i  32325  addltmulALT  32523  expgt0b  32899  cnre2csqlem  34069  tpr2rico  34071  satffunlem2lem1  35600  mclsax  35765  dfrdg4  36147  segconeq  36206  nn0prpwlem  36518  bj-bary1lem1  37518  poimirlem29  37852  fdc  37948  bfplem2  38026  atexchcvrN  39722  dalem3  39946  cdleme3h  40517  cdleme21ct  40611  oexpreposd  42598  cantnfresb  43587  omabs2  43595  naddwordnexlem4  43664  sbgoldbwt  48044  sbgoldbst  48045  nnsum4primesodd  48063  nnsum4primesoddALTV  48064  dignn0flhalflem1  48882