Theorem sylanr2 653

Description: A syllogism inference. (Contributed by NM, 9-Apr-2005.)

Hypotheses

Ref	Expression
sylanr2.1
sylanr2.2

Assertion

Ref	Expression
sylanr2

Proof of Theorem sylanr2

Step	Hyp	Ref	Expression
1		sylanr2.1	. . 3
2	1	anim2i 569	. 2
3		sylanr2.2	. 2
4	2, 3	sylan2 474	1

Syntax hints:  ->wi 4  /\wa 369

This theorem is referenced by:  adantrrl  723  adantrrr  724  1stconst  6888  2ndconst  6889  isfin7-2  8797  mulsub  10024  fzsubel  11748  expsub  12213  ramlb  14537  0ram  14538  ressmplvsca  18121  tgcl  19471  fgss2  20375  nmoid  21249  chirredlem4  27312  pridlc3  30470  stoweidlem34  31816

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