Theorem wefr 5628

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

Syntax hints:   → wi 4   Or wor 5545   Fr wfr 5588   We wwe 5590

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 5593

This theorem is referenced by:  wefrc  5632  wereu  5634  wereu2  5635  tz6.26  6320  wfi  6322  wfisg  6324  wfis2fg  6326  ordfr  6347  wexp  8109  wfrfun  8302  wfrresex  8303  wfr2a  8304  wfr1  8305  wofib  9498  wemapso  9504  wemapso2lem  9505  cflim2  10216  fpwwe2lem11  10594  fpwwe2lem12  10595  fpwwe2  10596  weiunwe  36457  welb  37730  fnwe2lem2  43040  onfrALTlem3  44534  onfrALTlem3VD  44876