Theorem wefr 5526

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

Assertion

Ref	Expression
wefr	⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴)

Proof of Theorem wefr

Step	Hyp	Ref	Expression
1		df-we 5496	. 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
2	1	simplbi 501	1 ⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴)

Syntax hints:   → wi 4   Or wor 5452   Fr wfr 5491   We wwe 5493

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

This theorem depends on definitions:  df-bi 210  df-an 400  df-we 5496

This theorem is referenced by:  wefrc  5530  wereu  5532  wereu2  5533  ordfr  6206  wexp  7875  wfrlem14  8046  wofib  9139  wemapso  9145  wemapso2lem  9146  cflim2  9842  fpwwe2lem11  10220  fpwwe2lem12  10221  fpwwe2  10222  welb  35580  fnwe2lem2  40520  onfrALTlem3  41778  onfrALTlem3VD  42121