Theorem 3syld 61

Description: Triple syllogism deduction. Deduction associated with 3syld 61. (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 48	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
4		3syld.3	. 2 ⊢ (𝜑 → (𝜃 → 𝜏))
5	3, 4	syld 48	1 ⊢ (𝜑 → (𝜓 → 𝜏))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  oaordi  8537  nnaordi  8610  fineqvlem  9233  dif1ennnALT  9244  rankr1ag  9781  cfslb2n  10267  fin23lem27  10327  gchpwdom  10672  prlem934  11035  axpre-sup  11171  cju  12231  xrub  13356  facavg  14357  mulcn2  15673  o1rlimmul  15696  coprm  16794  rpexp  16805  vdwnnlem3  17081  gexdvds  19700  cnpnei  23473  comppfsc  23742  alexsubALTlem3  24259  alexsubALTlem4  24260  iccntr  25032  cfil3i  25481  bcth3  25543  lgseisenlem2  27593  cusgredg  29834  uspgr2wlkeq  30055  ubthlem1  31295  staddi  32671  stadd3i  32673  addltmulALT  32871  expgt0b  33233  cnre2csqlem  34366  tpr2rico  34368  satffunlem2lem1  35935  mclsax  36100  dfrdg4  36482  segconeq  36541  nn0prpwlem  36892  bj-bary1lem1  38014  poimirlem29  38359  findcard4  38424  fdc  38456  bfplem2  38534  atexchcvrN  40274  dalem3  40498  cdleme3h  41069  cdleme21ct  41163  oexpreposd  43143  cantnfresb  44111  omabs2  44119  naddwordnexlem4  44188  sbgoldbwt  48602  sbgoldbst  48603  nnsum4primesodd  48621  nnsum4primesoddALTV  48622  dignn0flhalflem1  49454