Theorem sylanl1 650

Description: A syllogism inference. (Contributed by NM, 10-Mar-2005.)

Hypotheses

Ref	Expression
sylanl1.1
sylanl1.2

Assertion

Ref	Expression
sylanl1

Proof of Theorem sylanl1

Step	Hyp	Ref	Expression
1		sylanl1.1	. . 3
2	1	anim1i 568	. 2
3		sylanl1.2	. 2
4	2, 3	sylan 471	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  adantlll  717  adantllr  718  isocnv  6226  odi  7247  oeoelem  7266  mapxpen  7703  xadddilem  11515  pcqmul  14377  infpnlem1  14428  chpdmat  19342  neitr  19681  hausflimi  20481  nmoix  21236  nmoleub  21238  metdsre  21357  pthdepisspth  24576  extwwlkfab  25090  sspph  25770  unoplin  26839  hmoplin  26861  chirredlem1  27309  mdsymlem2  27323  foresf1o  27403  ordtconlem1  27906  heicant  30049  cnambfre  30063  itg2addnclem  30066  ftc1anclem5  30094  ftc1anc  30098  rrnequiv  30331  isfldidl  30465  ispridlc  30467  reccot  33152  rectan  33153

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

This theorem depends on definitions:  df-bi 185  df-an 371