Theorem weso 2937

Description: A well-ordering is a strict ordering.

Assertion

Ref	Expression
weso	|- (R We A -> R Or A)

Proof of Theorem weso

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

Syntax hints:   -> wi 3   Or wor 2836   Fr wfr 2912   We wwe 2913

This theorem is referenced by:  wecmpep 2938  wetrep 2939  wereu 2942

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 2931

Copyright terms: Public domain