Theorem sylsyld 56

Description: A double syllogism inference. (Contributed by Alan Sare, 20-Apr-2011.)

Hypotheses

Ref	Expression
sylsyld.1
sylsyld.2
sylsyld.3

Assertion

Ref	Expression
sylsyld

Proof of Theorem sylsyld

Step	Hyp	Ref	Expression
1		sylsyld.2	. 2
2		sylsyld.1	. . 3
3		sylsyld.3	. . 3
4	2, 3	syl 16	. 2
5	1, 4	syld 44	1

Syntax hints:  ->wi 4

This theorem is referenced by:  axc16gALT  2106  ax16g-o  2264  axc11-o  2281  trint0  4562  onfununi  7031  smoiun  7051  findcard2  7780  findcard3  7783  inficl  7905  en3lplem2  8053  r1sdom  8213  infxpenlem  8412  alephordi  8476  cardaleph  8491  pwsdompw  8605  cfslb2n  8669  isf32lem10  8763  axdc4lem  8856  zorn2lem2  8898  alephreg  8978  inar1  9174  tskuni  9182  grudomon  9216  nqereu  9328  ltleletr  9698  elfz0ubfz0  11807  ssnn0fi  12094  caubnd  13191  sqreulem  13192  bezoutlem1  14176  pcprendvds  14364  prmreclem3  14436  ptcmpfi  20314  ufilen  20431  fcfnei  20536  bcthlem5  21767  aaliou  22734  cusgrarn  24459  3cyclfrgrarn1  25012  n4cyclfrgra  25018  occon2  26206  occon3  26215  atexch  27300  sigaclci  28132  frmin  29322  idinside  29734  heibor1lem  30305  aomclem2  31001  leltletr  32318  ee02  33223  tratrb  33307  trsspwALT2  33617

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