Theorem wefr 5667

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

Syntax hints:   → wi 4   Or wor 5588   Fr wfr 5629   We wwe 5631

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 398  df-we 5634

This theorem is referenced by:  wefrc  5671  wereu  5673  wereu2  5674  tz6.26  6349  wfi  6352  wfisg  6355  wfis2fg  6358  ordfr  6380  wexp  8116  wfrlem14OLD  8322  wfrfun  8332  wfrresex  8333  wfr2a  8334  wfr1  8335  wofib  9540  wemapso  9546  wemapso2lem  9547  cflim2  10258  fpwwe2lem11  10636  fpwwe2lem12  10637  fpwwe2  10638  welb  36604  fnwe2lem2  41793  onfrALTlem3  43305  onfrALTlem3VD  43648