Theorem wefr 5394

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

Syntax hints:   → wi 4   Or wor 5322   Fr wfr 5360   We wwe 5362

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 199  df-an 388  df-we 5365

This theorem is referenced by:  wefrc  5398  wereu  5400  wereu2  5401  ordfr  6042  wexp  7628  wfrlem14  7771  wofib  8803  wemapso  8809  wemapso2lem  8810  cflim2  9482  fpwwe2lem12  9860  fpwwe2lem13  9861  fpwwe2  9862  welb  34486  fnwe2lem2  39081  onfrALTlem3  40331  onfrALTlem3VD  40674