Theorem syli 37

Description: Syllogism inference with common nested antecedent. (Contributed by NM, 4-Nov-2004.)

Hypotheses

Ref	Expression
syli.1
syli.2

Assertion

Ref	Expression
syli

Proof of Theorem syli

Step	Hyp	Ref	Expression
1		syli.1	. 2
2		syli.2	. . 3
3	2	com12 31	. 2
4	1, 3	sylcom 29	1

Syntax hints:  ->wi 4

This theorem is referenced by:  ibd  243  bija  355  equvini  2087  equveli  2088  equveliOLD  2089  2eu6  2383  rgen2a  2884  rexraleqim  3225  elreldm  5232  tz6.12c  5890  onminex  6642  rntpos  6987  smores  7042  seqomlem2  7135  f1domg  7555  php  7721  fodomnum  8459  carduniima  8498  cardmin  8960  negn0  11197  sqrmo  13085  grpomndo  25348  elghomlem2OLD  25364  isch3  26159  cgrtriv  29652  wl-lem-moexsb  30017

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