Metamath Proof Explorer

Theorem wefr

Description: A well-ordering is well-founded. (Contributed by NM, 22-Apr-1994)

Ref Expression
Assertion wefr 
|- ( R We A -> R Fr A )

Proof

Step Hyp Ref Expression
1 df-we 
 |-  ( R We A <-> ( R Fr A /\ R Or A ) )
2 1 simplbi 
 |-  ( R We A -> R Fr A )