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  8558  nnaordi  8630  fineqvlem  9270  dif1ennnALT  9283  xpfiOLD  9331  rankr1ag  9816  cfslb2n  10282  fin23lem27  10342  gchpwdom  10684  prlem934  11047  axpre-sup  11183  cju  12236  xrub  13328  facavg  14319  mulcn2  15612  o1rlimmul  15635  coprm  16730  rpexp  16741  vdwnnlem3  17017  gexdvds  19565  cnpnei  23202  comppfsc  23470  alexsubALTlem3  23987  alexsubALTlem4  23988  iccntr  24761  cfil3i  25221  bcth3  25283  lgseisenlem2  27339  cusgredg  29403  uspgr2wlkeq  29626  ubthlem1  30851  staddi  32227  stadd3i  32229  addltmulALT  32427  expgt0b  32795  cnre2csqlem  33941  tpr2rico  33943  satffunlem2lem1  35426  mclsax  35591  dfrdg4  35969  segconeq  36028  nn0prpwlem  36340  bj-bary1lem1  37329  poimirlem29  37673  fdc  37769  bfplem2  37847  atexchcvrN  39459  dalem3  39683  cdleme3h  40254  cdleme21ct  40348  oexpreposd  42371  cantnfresb  43348  omabs2  43356  naddwordnexlem4  43425  sbgoldbwt  47791  sbgoldbst  47792  nnsum4primesodd  47810  nnsum4primesoddALTV  47811  dignn0flhalflem1  48595