Theorem wefr 5631

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

Syntax hints:   → wi 4   Or wor 5548   Fr wfr 5591   We wwe 5593

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 5596

This theorem is referenced by:  wefrc  5635  wereu  5637  wereu2  5638  tz6.26  6323  wfi  6325  wfisg  6327  wfis2fg  6329  ordfr  6350  wexp  8112  wfrfun  8305  wfrresex  8306  wfr2a  8307  wfr1  8308  wofib  9505  wemapso  9511  wemapso2lem  9512  cflim2  10223  fpwwe2lem11  10601  fpwwe2lem12  10602  fpwwe2  10603  weiunwe  36464  welb  37737  fnwe2lem2  43047  onfrALTlem3  44541  onfrALTlem3VD  44883