MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  wefr Structured version   Unicode version

Theorem wefr 4821
Description: A well-ordering is well-founded. (Contributed by NM, 22-Apr-1994.)
Assertion
Ref Expression
wefr  |-  ( R  We  A  ->  R  Fr  A )

Proof of Theorem wefr
StepHypRef Expression
1 df-we 4792 . 2  |-  ( R  We  A  <->  ( R  Fr  A  /\  R  Or  A ) )
21simplbi 460 1  |-  ( R  We  A  ->  R  Fr  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    Or wor 4751    Fr wfr 4787    We wwe 4789
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 185  df-an 371  df-we 4792
This theorem is referenced by:  wefrc  4825  wereu  4827  wereu2  4828  ordfr  4845  wexp  6799  wofib  7874  wemapso  7880  wemapso2OLD  7881  wemapso2lem  7882  cflim2  8547  fpwwe2lem12  8923  fpwwe2lem13  8924  fpwwe2  8925  wfrlem14  27904  welb  28801  fnwe2lem2  29575  onfrALTlem3  31607  onfrALTlem3VD  31978
  Copyright terms: Public domain W3C validator