Theorem wefr 5613

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

Syntax hints:   → wi 4   Or wor 5530   Fr wfr 5573   We wwe 5575

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 5578

This theorem is referenced by:  wefrc  5617  wereu  5619  wereu2  5620  tz6.26  6304  wfi  6306  wfisg  6308  wfis2fg  6310  ordfr  6331  wexp  8072  wfrfun  8265  wfrresex  8266  wfr2a  8267  wfr1  8268  wofib  9452  wemapso  9458  wemapso2lem  9459  cflim2  10175  fpwwe2lem11  10554  fpwwe2lem12  10555  fpwwe2  10556  ons2ind  28254  weiunwe  36642  welb  37906  fnwe2lem2  43330  onfrALTlem3  44822  onfrALTlem3VD  45164