Theorem syl6ci 65

Description: A syllogism inference combined with contraction. (Contributed by Alan Sare, 18-Mar-2012.)

Hypotheses

Ref	Expression
syl6ci.1
syl6ci.2
syl6ci.3

Assertion

Ref	Expression
syl6ci

Proof of Theorem syl6ci

Step	Hyp	Ref	Expression
1		syl6ci.1	. 2
2		syl6ci.2	. . 3
3	2	a1d 25	. 2
4		syl6ci.3	. 2
5	1, 3, 4	syl6c 64	1

Syntax hints:  ->wi 4

This theorem is referenced by:  ordelord  4905  f1dmex  6770  omeulem2  7251  2pwuninel  7692  isumrpcl  13655  kqfvima  20231  caubl  21746  frgrawopreglem2  25045  soseq  29334  btwnconn1lem12  29748  sbcim2g  33309  ee21an  33529

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