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  8583  nnaordi  8655  fineqvlem  9296  dif1ennnALT  9309  xpfiOLD  9357  rankr1ag  9840  cfslb2n  10306  fin23lem27  10366  gchpwdom  10708  prlem934  11071  axpre-sup  11207  cju  12260  xrub  13351  facavg  14337  mulcn2  15629  o1rlimmul  15652  coprm  16745  rpexp  16756  vdwnnlem3  17031  gexdvds  19617  cnpnei  23288  comppfsc  23556  alexsubALTlem3  24073  alexsubALTlem4  24074  iccntr  24857  cfil3i  25317  bcth3  25379  lgseisenlem2  27435  cusgredg  29456  uspgr2wlkeq  29679  ubthlem1  30899  staddi  32275  stadd3i  32277  addltmulALT  32475  expgt0b  32823  cnre2csqlem  33871  tpr2rico  33873  satffunlem2lem1  35389  mclsax  35554  dfrdg4  35933  segconeq  35992  nn0prpwlem  36305  bj-bary1lem1  37294  poimirlem29  37636  fdc  37732  bfplem2  37810  atexchcvrN  39423  dalem3  39647  cdleme3h  40218  cdleme21ct  40312  oexpreposd  42336  cantnfresb  43314  omabs2  43322  naddwordnexlem4  43391  sbgoldbwt  47702  sbgoldbst  47703  nnsum4primesodd  47721  nnsum4primesoddALTV  47722  dignn0flhalflem1  48465