Theorem wefr 5668

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

Syntax hints:   → wi 4   Or wor 5589   Fr wfr 5630   We wwe 5632

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 395  df-we 5635

This theorem is referenced by:  wefrc  5672  wereu  5674  wereu2  5675  tz6.26  6355  wfi  6358  wfisg  6361  wfis2fg  6364  ordfr  6386  wexp  8135  wfrlem14OLD  8343  wfrfun  8353  wfrresex  8354  wfr2a  8355  wfr1  8356  wofib  9570  wemapso  9576  wemapso2lem  9577  cflim2  10288  fpwwe2lem11  10666  fpwwe2lem12  10667  fpwwe2  10668  welb  37340  fnwe2lem2  42617  onfrALTlem3  44125  onfrALTlem3VD  44468