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

Theorem wefr 4812
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 4783 . 2  |-  ( R  We  A  <->  ( R  Fr  A  /\  R  Or  A ) )
21simplbi 458 1  |-  ( R  We  A  ->  R  Fr  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    Or wor 4742    Fr wfr 4778    We wwe 4780
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 369  df-we 4783
This theorem is referenced by:  wefrc  4816  wereu  4818  wereu2  4819  ordfr  5424  wexp  6897  wfrlem14  7033  wofib  8003  wemapso  8009  wemapso2OLD  8010  wemapso2lem  8011  cflim2  8674  fpwwe2lem12  9048  fpwwe2lem13  9049  fpwwe2  9050  welb  31489  fnwe2lem2  35339  onfrALTlem3  36320  onfrALTlem3VD  36698
  Copyright terms: Public domain W3C validator