Theorem wefr 2945

Description: A well-ordering is founded.

Assertion

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

Proof of Theorem wefr

Step	Hyp	Ref	Expression
1		df-we 2940	. 2 |- (R We A <-> (R Fr A /\ R Or A))
2	1	pm3.26bi 322	1 |- (R We A -> R Fr A)

Syntax hints:   -> wi 3   Or wor 2845   Fr wfr 2921   We wwe 2922

This theorem is referenced by:  wefrc 2949  wereu 2951  ordfr 2969

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-we 2940

Copyright terms: Public domain