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  8565  nnaordi  8638  fineqvlem  9268  dif1ennnALT  9279  rankr1ag  9820  cfslb2n  10356  fin23lem27  10416  gchpwdom  10765  prlem934  11128  axpre-sup  11264  cju  12326  xrub  13452  facavg  14455  mulcn2  15775  o1rlimmul  15798  coprm  16899  rpexp  16910  vdwnnlem3  17187  gexdvds  19810  cnpnei  23594  comppfsc  23863  alexsubALTlem3  24380  alexsubALTlem4  24381  iccntr  25153  cfil3i  25602  bcth3  25664  lgseisenlem2  27715  fltoprm  28007  cusgredg  30017  uspgr2wlkeq  30238  ubthlem1  31484  staddi  32860  stadd3i  32862  addltmulALT  33102  expgt0b  33461  cnre2csqlem  34595  tpr2rico  34597  satffunlem2lem1  36290  mclsax  36455  dfrdg4  36842  segconeq  36902  nn0prpwlem  37237  bj-bary1lem1  38372  poimirlem29  38707  findcard4  38772  fdc  38819  bfplem2  38897  atexchcvrN  40637  dalem3  40861  cdleme3h  41432  cdleme21ct  41526  oexpreposd  43519  cantnfresb  44466  omabs2  44474  naddwordnexlem4  44543  sbgoldbwt  49014  sbgoldbst  49015  nnsum4primesodd  49033  nnsum4primesoddALTV  49034  dignn0flhalflem1  49866