Theorem sylanl2 651

Description: A syllogism inference. (Contributed by NM, 1-Jan-2005.)

Hypotheses

Ref	Expression
sylanl2.1
sylanl2.2

Assertion

Ref	Expression
sylanl2

Proof of Theorem sylanl2

Step	Hyp	Ref	Expression
1		sylanl2.1	. . 3
2	1	anim2i 569	. 2
3		sylanl2.2	. 2
4	2, 3	sylan 471	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  mpanlr1  686  adantlrl  719  adantlrr  720  oesuclem  7194  oelim  7203  mulsub  10024  divsubdiv  10285  vdwlem12  14510  dpjidcl  17107  dpjidclOLD  17114  mplbas2  18134  monmat2matmon  19325  bwth  19910  cnextfun  20564  elbl4  21079  metucnOLD  21091  metucn  21092  dvradcnv  22816  dchrisum0lem2a  23702  axcontlem4  24270  cnlnadjlem2  26987  chirredlem2  27310  mdsymlem5  27326  sibfof  28282  unichnidl  30428  dmncan2  30474  jm2.26  30944  radcnvrat  31195  lcmneg  31209  binomcxplemnotnn0  31261  dvnmptdivc  31735  fourierdlem64  31953  fourierdlem74  31963  fourierdlem75  31964  fourierdlem83  31972  etransclem35  32052  cvrexchlem  35143

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