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  8339  nnaordi  8411  fineqvlem  8966  dif1enALT  8980  xpfi  9015  rankr1ag  9491  cfslb2n  9955  fin23lem27  10015  gchpwdom  10357  prlem934  10720  axpre-sup  10856  cju  11899  xrub  12975  facavg  13943  mulcn2  15233  o1rlimmul  15256  coprm  16344  rpexp  16355  vdwnnlem3  16626  gexdvds  19104  cnpnei  22323  comppfsc  22591  alexsubALTlem3  23108  alexsubALTlem4  23109  iccntr  23890  cfil3i  24338  bcth3  24400  lgseisenlem2  26429  cusgredg  27694  uspgr2wlkeq  27915  ubthlem1  29133  staddi  30509  stadd3i  30511  addltmulALT  30709  cnre2csqlem  31762  tpr2rico  31764  satffunlem2lem1  33266  mclsax  33431  dfrdg4  34180  segconeq  34239  nn0prpwlem  34438  bj-bary1lem1  35409  poimirlem29  35733  fdc  35830  bfplem2  35908  atexchcvrN  37381  dalem3  37605  cdleme3h  38176  cdleme21ct  38270  oexpreposd  40242  sbgoldbwt  45117  sbgoldbst  45118  nnsum4primesodd  45136  nnsum4primesoddALTV  45137  dignn0flhalflem1  45849