NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  expr Unicode version

Theorem expr 598
Description: Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)
Hypothesis
Ref Expression
expr.1
Assertion
Ref Expression
expr

Proof of Theorem expr
StepHypRef Expression
1 expr.1 . . 3
21exp32 588 . 2
32imp 418 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   wa 358
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
This theorem is referenced by:  rexlimdvaa  2739  ncfinraise  4481  ncfinlower  4483  tfin11  4493  tfinpw1  4494  tfinltfinlem1  4500  tfinltfin  4501  evenodddisj  4516  nnpweq  4523  sfin112  4529  sfindbl  4530  tfinnn  4534  vfinspss  4551  funiunfv  5467  erth  5968  enprmaplem3  6078  peano4nc  6150  ncssfin  6151  nntccl  6170  leltctr  6212  tlecg  6230  nchoicelem6  6294  nchoicelem8  6296  nchoicelem17  6305  fnfrec  6320
  Copyright terms: Public domain W3C validator