Theorem wefr 5616

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

Syntax hints:   → wi 4   Or wor 5533   Fr wfr 5576   We wwe 5578

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 5581

This theorem is referenced by:  wefrc  5620  wereu  5622  wereu2  5623  tz6.26  6307  wfi  6309  wfisg  6311  wfis2fg  6313  ordfr  6334  wexp  8075  wfrfun  8268  wfrresex  8269  wfr2a  8270  wfr1  8271  wofib  9455  wemapso  9461  wemapso2lem  9462  cflim2  10180  fpwwe2lem11  10559  fpwwe2lem12  10560  fpwwe2  10561  ons2ind  28285  weiunwe  36671  welb  38077  fnwe2lem2  43503  onfrALTlem3  44995  onfrALTlem3VD  45337