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

Theorem wefr 4706
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 4677 . 2  |-  ( R  We  A  <->  ( R  Fr  A  /\  R  Or  A ) )
21simplbi 457 1  |-  ( R  We  A  ->  R  Fr  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    Or wor 4636    Fr wfr 4672    We wwe 4674
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 4677
This theorem is referenced by:  wefrc  4710  wereu  4712  wereu2  4713  ordfr  4730  wexp  6685  wofib  7755  wemapso  7761  wemapso2OLD  7762  wemapso2lem  7763  cflim2  8428  fpwwe2lem12  8804  fpwwe2lem13  8805  fpwwe2  8806  wfrlem14  27650  welb  28539  fnwe2lem2  29313  onfrALTlem3  31068  onfrALTlem3VD  31440
  Copyright terms: Public domain W3C validator