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  8536  nnaordi  8609  fineqvlem  9239  dif1ennnALT  9250  rankr1ag  9787  cfslb2n  10273  fin23lem27  10333  gchpwdom  10682  prlem934  11045  axpre-sup  11181  cju  12241  xrub  13367  facavg  14368  mulcn2  15686  o1rlimmul  15709  coprm  16805  rpexp  16816  vdwnnlem3  17092  gexdvds  19714  cnpnei  23492  comppfsc  23761  alexsubALTlem3  24278  alexsubALTlem4  24279  iccntr  25051  cfil3i  25500  bcth3  25562  lgseisenlem2  27615  cusgredg  29887  uspgr2wlkeq  30108  ubthlem1  31354  staddi  32730  stadd3i  32732  addltmulALT  32930  expgt0b  33290  cnre2csqlem  34423  tpr2rico  34425  satffunlem2lem1  35986  mclsax  36151  dfrdg4  36533  segconeq  36593  nn0prpwlem  36944  bj-bary1lem1  38066  poimirlem29  38401  findcard4  38466  fdc  38498  bfplem2  38576  atexchcvrN  40316  dalem3  40540  cdleme3h  41111  cdleme21ct  41205  oexpreposd  43200  cantnfresb  44168  omabs2  44176  naddwordnexlem4  44245  sbgoldbwt  48696  sbgoldbst  48697  nnsum4primesodd  48715  nnsum4primesoddALTV  48716  dignn0flhalflem1  49548