Theorem wefr 5690

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

Syntax hints:   → wi 4   Or wor 5606   Fr wfr 5649   We wwe 5651

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 5654

This theorem is referenced by:  wefrc  5694  wereu  5696  wereu2  5697  tz6.26  6379  wfi  6382  wfisg  6385  wfis2fg  6388  ordfr  6410  wexp  8171  wfrlem14OLD  8378  wfrfun  8388  wfrresex  8389  wfr2a  8390  wfr1  8391  wofib  9614  wemapso  9620  wemapso2lem  9621  cflim2  10332  fpwwe2lem11  10710  fpwwe2lem12  10711  fpwwe2  10712  weiunwe  36435  welb  37696  fnwe2lem2  43008  onfrALTlem3  44515  onfrALTlem3VD  44858