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  8129  wfrlem14OLD  8336  wfrfun  8346  wfrresex  8347  wfr2a  8348  wfr1  8349  wofib  9559  wemapso  9565  wemapso2lem  9566  cflim2  10277  fpwwe2lem11  10655  fpwwe2lem12  10656  fpwwe2  10657  weiunwe  36487  welb  37760  fnwe2lem2  43075  onfrALTlem3  44569  onfrALTlem3VD  44911