Metamath Proof Explorer


Theorem ordpss

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

Ref Expression
Assertion ordpss ( Ord 𝐵 → ( 𝐴𝐵𝐴𝐵 ) )

Proof

Step Hyp Ref Expression
1 ordelord ( ( Ord 𝐵𝐴𝐵 ) → Ord 𝐴 )
2 1 ex ( Ord 𝐵 → ( 𝐴𝐵 → Ord 𝐴 ) )
3 2 ancrd ( Ord 𝐵 → ( 𝐴𝐵 → ( Ord 𝐴𝐴𝐵 ) ) )
4 ordelpss ( ( Ord 𝐴 ∧ Ord 𝐵 ) → ( 𝐴𝐵𝐴𝐵 ) )
5 4 ancoms ( ( Ord 𝐵 ∧ Ord 𝐴 ) → ( 𝐴𝐵𝐴𝐵 ) )
6 5 biimpd ( ( Ord 𝐵 ∧ Ord 𝐴 ) → ( 𝐴𝐵𝐴𝐵 ) )
7 6 expimpd ( Ord 𝐵 → ( ( Ord 𝐴𝐴𝐵 ) → 𝐴𝐵 ) )
8 3 7 syld ( Ord 𝐵 → ( 𝐴𝐵𝐴𝐵 ) )