Theorem 3syld 55

Description: Triple syllogism deduction. (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 44	. 2
4		3syld.3	. 2
5	3, 4	syld 44	1

Syntax hints:  ->wi 4

This theorem is referenced by:  oaordi  7214  nnaordi  7286  fineqvlem  7754  dif1enOLD  7772  dif1en  7773  xpfi  7811  rankr1ag  8241  cfslb2n  8669  fin23lem27  8729  gchpwdom  9069  prlem934  9432  axpre-sup  9567  cju  10557  xrub  11532  facavg  12379  mulcn2  13418  o1rlimmul  13441  coprm  14241  rpexp  14261  vdwnnlem3  14515  gexdvds  16604  cnpnei  19765  comppfsc  20033  alexsubALTlem3  20549  alexsubALTlem4  20550  iccntr  21326  cfil3i  21708  bcth3  21770  lgseisenlem2  23625  usgrasscusgra  24483  usg2wlkeq  24708  nbhashuvtx1  24915  frgrawopreglem4  25047  ubthlem1  25786  staddi  27165  stadd3i  27167  addltmulALT  27365  cnre2csqlem  27892  tpr2rico  27894  mclsax  28929  dfrdg4  29600  segconeq  29660  nn0prpwlem  30140  fdc  30238  bfplem2  30319  bj-bary1lem1  34680  atexchcvrN  35164  dalem3  35388  cdleme3h  35960  cdleme21ct  36055

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7