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

Syntax hints:   → wi 4   Or wor 5525   Fr wfr 5566   We wwe 5568

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 206  df-an 397  df-we 5571

This theorem is referenced by:  wefrc  5608  wereu  5610  wereu2  5611  tz6.26  6280  wfi  6283  wfisg  6286  wfis2fg  6289  ordfr  6311  wexp  8030  wfrlem14OLD  8215  wfrfun  8225  wfrresex  8226  wfr2a  8227  wfr1  8228  wofib  9394  wemapso  9400  wemapso2lem  9401  cflim2  10112  fpwwe2lem11  10490  fpwwe2lem12  10491  fpwwe2  10492  welb  35992  fnwe2lem2  41127  onfrALTlem3  42474  onfrALTlem3VD  42817