Theorem wefr 5615

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

Syntax hints:   → wi 4   Or wor 5532   Fr wfr 5575   We wwe 5577

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 5580

This theorem is referenced by:  wefrc  5619  wereu  5621  wereu2  5622  tz6.26  6306  wfi  6308  wfisg  6310  wfis2fg  6312  ordfr  6333  wexp  8074  wfrfun  8267  wfrresex  8268  wfr2a  8269  wfr1  8270  wofib  9454  wemapso  9460  wemapso2lem  9461  cflim2  10177  fpwwe2lem11  10556  fpwwe2lem12  10557  fpwwe2  10558  ons2ind  28275  weiunwe  36665  welb  37939  fnwe2lem2  43360  onfrALTlem3  44852  onfrALTlem3VD  45194