Theorem wefr 5604

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

Syntax hints:   → wi 4   Or wor 5521   Fr wfr 5564   We wwe 5566

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 5569

This theorem is referenced by:  wefrc  5608  wereu  5610  wereu2  5611  tz6.26  6294  wfi  6296  wfisg  6298  wfis2fg  6300  ordfr  6321  wexp  8060  wfrfun  8253  wfrresex  8254  wfr2a  8255  wfr1  8256  wofib  9431  wemapso  9437  wemapso2lem  9438  cflim2  10154  fpwwe2lem11  10532  fpwwe2lem12  10533  fpwwe2  10534  weiunwe  36513  welb  37775  fnwe2lem2  43143  onfrALTlem3  44636  onfrALTlem3VD  44978