Theorem 3syld 60

Description: Triple syllogism deduction. Deduction associated with 3syld 60. (Contributed by Jeff Hankins, 4-Aug-2009.)

Hypotheses

Ref	Expression
3syld.1	|- ( ph -> ( ps -> ch ) )
3syld.2	|- ( ph -> ( ch -> th ) )
3syld.3	|- ( ph -> ( th -> ta ) )

Assertion

Ref	Expression
3syld	|- ( ph -> ( ps -> ta ) )

Proof of Theorem 3syld

Step	Hyp	Ref	Expression
1		3syld.1	. . 3 |- ( ph -> ( ps -> ch ) )
2		3syld.2	. . 3 |- ( ph -> ( ch -> th ) )
3	1, 2	syld 47	. 2 |- ( ph -> ( ps -> th ) )
4		3syld.3	. 2 |- ( ph -> ( th -> ta ) )
5	3, 4	syld 47	1 |- ( ph -> ( ps -> ta ) )

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  7626  nnaordi  7698  fineqvlem  8174  dif1en  8193  xpfi  8231  rankr1ag  8665  cfslb2n  9090  fin23lem27  9150  gchpwdom  9492  prlem934  9855  axpre-sup  9990  cju  11016  xrub  12142  facavg  13088  mulcn2  14326  o1rlimmul  14349  coprm  15423  rpexp  15432  vdwnnlem3  15701  gexdvds  17999  cnpnei  21068  comppfsc  21335  alexsubALTlem3  21853  alexsubALTlem4  21854  iccntr  22624  cfil3i  23067  bcth3  23128  lgseisenlem2  25101  cusgredg  26320  uspgr2wlkeq  26542  ubthlem1  27726  staddi  29105  stadd3i  29107  addltmulALT  29305  cnre2csqlem  29956  tpr2rico  29958  mclsax  31466  dfrdg4  32058  segconeq  32117  nn0prpwlem  32317  bj-bary1lem1  33161  poimirlem29  33438  fdc  33541  bfplem2  33622  atexchcvrN  34726  dalem3  34950  cdleme3h  35522  cdleme21ct  35617  sbgoldbwt  41665  sbgoldbst  41666  nnsum4primesodd  41684  nnsum4primesoddALTV  41685  dignn0flhalflem1  42409