Theorem wefr 5678

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

Syntax hints:   → wi 4   Or wor 5595   Fr wfr 5637   We wwe 5639

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 5642

This theorem is referenced by:  wefrc  5682  wereu  5684  wereu2  5685  tz6.26  6369  wfi  6372  wfisg  6375  wfis2fg  6378  ordfr  6400  wexp  8153  wfrlem14OLD  8360  wfrfun  8370  wfrresex  8371  wfr2a  8372  wfr1  8373  wofib  9582  wemapso  9588  wemapso2lem  9589  cflim2  10300  fpwwe2lem11  10678  fpwwe2lem12  10679  fpwwe2  10680  weiunwe  36451  welb  37722  fnwe2lem2  43039  onfrALTlem3  44541  onfrALTlem3VD  44884