Theorem wefr 5675

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

Syntax hints:   → wi 4   Or wor 5591   Fr wfr 5634   We wwe 5636

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 5639

This theorem is referenced by:  wefrc  5679  wereu  5681  wereu2  5682  tz6.26  6368  wfi  6371  wfisg  6374  wfis2fg  6377  ordfr  6399  wexp  8155  wfrlem14OLD  8362  wfrfun  8372  wfrresex  8373  wfr2a  8374  wfr1  8375  wofib  9585  wemapso  9591  wemapso2lem  9592  cflim2  10303  fpwwe2lem11  10681  fpwwe2lem12  10682  fpwwe2  10683  weiunwe  36470  welb  37743  fnwe2lem2  43063  onfrALTlem3  44564  onfrALTlem3VD  44907