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  8472  nnaordi  8545  fineqvlem  9167  dif1ennnALT  9178  rankr1ag  9718  cfslb2n  10182  fin23lem27  10242  gchpwdom  10585  prlem934  10948  axpre-sup  11084  cju  12147  xrub  13256  facavg  14255  mulcn2  15550  o1rlimmul  15573  coprm  16673  rpexp  16684  vdwnnlem3  16960  gexdvds  19551  cnpnei  23248  comppfsc  23516  alexsubALTlem3  24033  alexsubALTlem4  24034  iccntr  24806  cfil3i  25255  bcth3  25317  lgseisenlem2  27358  cusgredg  29512  uspgr2wlkeq  29733  ubthlem1  30960  staddi  32336  stadd3i  32338  addltmulALT  32536  expgt0b  32910  cnre2csqlem  34103  tpr2rico  34105  satffunlem2lem1  35641  mclsax  35806  dfrdg4  36188  segconeq  36247  nn0prpwlem  36559  bj-bary1lem1  37680  poimirlem29  38025  fdc  38121  bfplem2  38199  atexchcvrN  39941  dalem3  40165  cdleme3h  40736  cdleme21ct  40830  oexpreposd  42808  cantnfresb  43778  omabs2  43786  naddwordnexlem4  43855  sbgoldbwt  48276  sbgoldbst  48277  nnsum4primesodd  48295  nnsum4primesoddALTV  48296  dignn0flhalflem1  49114