Theorem ordpss

Description: ordelpss with an antecedent removed. (Contributed by Andrew Salmon, 25-Jul-2011)

	Ref	Expression
Assertion	ordpss	|- ( Ord B -> ( A e. B -> A C. B ) )

Proof

Step	Hyp	Ref	Expression
1		ordelord	|- ( ( Ord B /\ A e. B ) -> Ord A )
2	1	ex	|- ( Ord B -> ( A e. B -> Ord A ) )
3	2	ancrd	|- ( Ord B -> ( A e. B -> ( Ord A /\ A e. B ) ) )
4		ordelpss	|- ( ( Ord A /\ Ord B ) -> ( A e. B <-> A C. B ) )
5	4	ancoms	|- ( ( Ord B /\ Ord A ) -> ( A e. B <-> A C. B ) )
6	5	biimpd	|- ( ( Ord B /\ Ord A ) -> ( A e. B -> A C. B ) )
7	6	expimpd	|- ( Ord B -> ( ( Ord A /\ A e. B ) -> A C. B ) )
8	3 7	syld	|- ( Ord B -> ( A e. B -> A C. B ) )