Theorem wefr 5644

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 5608	. 2 ⊢ (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴))
2	1	simplbi 497	1 ⊢ (𝑅 We 𝐴 → 𝑅 Fr 𝐴)

Syntax hints:   → wi 4   Or wor 5560   Fr wfr 5603   We wwe 5605

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 207  df-an 396  df-we 5608

This theorem is referenced by:  wefrc  5648  wereu  5650  wereu2  5651  tz6.26  6336  wfi  6339  wfisg  6342  wfis2fg  6345  ordfr  6367  wexp  8127  wfrlem14OLD  8334  wfrfun  8344  wfrresex  8345  wfr2a  8346  wfr1  8347  wofib  9557  wemapso  9563  wemapso2lem  9564  cflim2  10275  fpwwe2lem11  10653  fpwwe2lem12  10654  fpwwe2  10655  weiunwe  36433  welb  37706  fnwe2lem2  43022  onfrALTlem3  44517  onfrALTlem3VD  44859