Theorem wefr 5579

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

Syntax hints:   → wi 4   Or wor 5502   Fr wfr 5541   We wwe 5543

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 206  df-an 397  df-we 5546

This theorem is referenced by:  wefrc  5583  wereu  5585  wereu2  5586  tz6.26  6250  wfi  6253  wfisg  6256  wfis2fg  6259  ordfr  6281  wexp  7971  wfrlem14OLD  8153  wfrfun  8163  wfrresex  8164  wfr2a  8165  wfr1  8166  wofib  9304  wemapso  9310  wemapso2lem  9311  cflim2  10019  fpwwe2lem11  10397  fpwwe2lem12  10398  fpwwe2  10399  welb  35894  fnwe2lem2  40876  onfrALTlem3  42164  onfrALTlem3VD  42507