New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > 3expia | Unicode version |
Description: Exportation from triple conjunction. (Contributed by NM, 19-May-2007.) |
Ref | Expression |
---|---|
3exp.1 |
Ref | Expression |
---|---|
3expia |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp.1 | . . 3 | |
2 | 1 | 3exp 1150 | . 2 |
3 | 2 | imp 418 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 358 w3a 934 |
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 df-3an 936 |
This theorem is referenced by: mp3an3 1266 3gencl 2889 moi 3019 ltfintri 4466 tfindi 4496 nnadjoin 4520 nnpweq 4523 sfintfin 4532 tfinnn 4534 sfinltfin 4535 vfintle 4546 suc11nnc 4558 phi11lem1 4595 3optocl 4840 ndmovord 5620 ov2gf 5711 antird 5928 iserd 5942 mapvalg 6009 enprmaplem5 6080 enprmaplem6 6081 nclenc 6222 lenc 6223 nclenn 6249 nchoicelem17 6305 nchoicelem19 6307 fnfreclem3 6319 |
Copyright terms: Public domain | W3C validator |