Theorem wefr 5239

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

Syntax hints:   → wi 4   Or wor 5169   Fr wfr 5205   We wwe 5207

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 197  df-an 383  df-we 5210

This theorem is referenced by:  wefrc  5243  wereu  5245  wereu2  5246  ordfr  5881  wexp  7442  wfrlem14  7581  wofib  8606  wemapso  8612  wemapso2lem  8613  cflim2  9287  fpwwe2lem12  9665  fpwwe2lem13  9666  fpwwe2  9667  welb  33863  fnwe2lem2  38147  onfrALTlem3  39284  onfrALTlem3VD  39645