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  8546  nnaordi  8618  fineqvlem  9262  dif1ennnALT  9277  xpfiOLD  9318  rankr1ag  9797  cfslb2n  10263  fin23lem27  10323  gchpwdom  10665  prlem934  11028  axpre-sup  11164  cju  12208  xrub  13291  facavg  14261  mulcn2  15540  o1rlimmul  15563  coprm  16648  rpexp  16659  vdwnnlem3  16930  gexdvds  19452  cnpnei  22768  comppfsc  23036  alexsubALTlem3  23553  alexsubALTlem4  23554  iccntr  24337  cfil3i  24786  bcth3  24848  lgseisenlem2  26879  cusgredg  28681  uspgr2wlkeq  28903  ubthlem1  30123  staddi  31499  stadd3i  31501  addltmulALT  31699  cnre2csqlem  32890  tpr2rico  32892  satffunlem2lem1  34395  mclsax  34560  dfrdg4  34923  segconeq  34982  nn0prpwlem  35207  bj-bary1lem1  36192  poimirlem29  36517  fdc  36613  bfplem2  36691  atexchcvrN  38311  dalem3  38535  cdleme3h  39106  cdleme21ct  39200  oexpreposd  41212  cantnfresb  42074  omabs2  42082  naddwordnexlem4  42152  sbgoldbwt  46445  sbgoldbst  46446  nnsum4primesodd  46464  nnsum4primesoddALTV  46465  dignn0flhalflem1  47301