Theorem wefr 5609

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

Syntax hints:   → wi 4   Or wor 5526   Fr wfr 5569   We wwe 5571

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 5574

This theorem is referenced by:  wefrc  5613  wereu  5615  wereu2  5616  tz6.26  6295  wfi  6297  wfisg  6299  wfis2fg  6301  ordfr  6322  wexp  8063  wfrfun  8256  wfrresex  8257  wfr2a  8258  wfr1  8259  wofib  9437  wemapso  9443  wemapso2lem  9444  cflim2  10157  fpwwe2lem11  10535  fpwwe2lem12  10536  fpwwe2  10537  weiunwe  36463  welb  37736  fnwe2lem2  43044  onfrALTlem3  44538  onfrALTlem3VD  44880