Theorem wefr 5652

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

Syntax hints:   → wi 4   Or wor 5569   Fr wfr 5612   We wwe 5614

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 210  df-an 401  df-we 5617

This theorem is referenced by:  wefrc  5656  wereu  5658  wereu2  5659  tz6.26  6349  wfi  6351  wfisg  6353  wfis2fg  6355  ordfr  6376  wexp  8126  wfrfun  8320  wfrresex  8321  wfr2a  8322  wfr1  8323  wofib  9507  wemapso  9513  wemapso2lem  9514  cflim2  10247  fpwwe2lem11  10626  fpwwe2lem12  10627  fpwwe2  10628  ons2ind  28434  weiunwe  36903  welb  38310  fnwe2lem2  43705  onfrALTlem3  45180  onfrALTlem3VD  45522