# Metamath Proof Explorer

## Theorem ordpss

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

Ref Expression
Assertion ordpss ${⊢}\mathrm{Ord}{B}\to \left({A}\in {B}\to {A}\subset {B}\right)$

### Proof

Step Hyp Ref Expression
1 ordelord ${⊢}\left(\mathrm{Ord}{B}\wedge {A}\in {B}\right)\to \mathrm{Ord}{A}$
2 1 ex ${⊢}\mathrm{Ord}{B}\to \left({A}\in {B}\to \mathrm{Ord}{A}\right)$
3 2 ancrd ${⊢}\mathrm{Ord}{B}\to \left({A}\in {B}\to \left(\mathrm{Ord}{A}\wedge {A}\in {B}\right)\right)$
4 ordelpss ${⊢}\left(\mathrm{Ord}{A}\wedge \mathrm{Ord}{B}\right)\to \left({A}\in {B}↔{A}\subset {B}\right)$
5 4 ancoms ${⊢}\left(\mathrm{Ord}{B}\wedge \mathrm{Ord}{A}\right)\to \left({A}\in {B}↔{A}\subset {B}\right)$
6 5 biimpd ${⊢}\left(\mathrm{Ord}{B}\wedge \mathrm{Ord}{A}\right)\to \left({A}\in {B}\to {A}\subset {B}\right)$
7 6 expimpd ${⊢}\mathrm{Ord}{B}\to \left(\left(\mathrm{Ord}{A}\wedge {A}\in {B}\right)\to {A}\subset {B}\right)$
8 3 7 syld ${⊢}\mathrm{Ord}{B}\to \left({A}\in {B}\to {A}\subset {B}\right)$