Theorem wefr 5656

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

Syntax hints:   → wi 4   Or wor 5577   Fr wfr 5618   We wwe 5620

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 5623

This theorem is referenced by:  wefrc  5660  wereu  5662  wereu2  5663  tz6.26  6334  wfi  6337  wfisg  6340  wfis2fg  6343  ordfr  6365  wexp  8095  wfrlem14OLD  8301  wfrfun  8311  wfrresex  8312  wfr2a  8313  wfr1  8314  wofib  9519  wemapso  9525  wemapso2lem  9526  cflim2  10237  fpwwe2lem11  10615  fpwwe2lem12  10616  fpwwe2  10617  welb  36393  fnwe2lem2  41550  onfrALTlem3  43062  onfrALTlem3VD  43405