Metamath Proof Explorer


Theorem ordpss

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

Ref Expression
Assertion ordpss Ord B A B A B

Proof

Step Hyp Ref Expression
1 ordelord Ord B A B Ord A
2 1 ex Ord B A B Ord A
3 2 ancrd Ord B A B Ord A A B
4 ordelpss Ord A Ord B A B A B
5 4 ancoms Ord B Ord A A B A B
6 5 biimpd Ord B Ord A A B A B
7 6 expimpd Ord B Ord A A B A B
8 3 7 syld Ord B A B A B