New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > expr | Unicode version |
Description: Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.) |
Ref | Expression |
---|---|
expr.1 |
Ref | Expression |
---|---|
expr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | expr.1 | . . 3 | |
2 | 1 | exp32 588 | . 2 |
3 | 2 | imp 418 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 358 |
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 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 |