New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > 3expa | Unicode version |
Description: Exportation from triple to double conjunction. (Contributed by NM, 20-Aug-1995.) |
Ref | Expression |
---|---|
3exp.1 |
Ref | Expression |
---|---|
3expa |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp.1 | . . 3 | |
2 | 1 | 3exp 1150 | . 2 |
3 | 2 | imp31 421 | 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: 3anidm23 1241 mp3an2 1265 mpd3an3 1278 rgen3 2711 moi2 3017 sbc3ie 3115 preq12bg 4128 eladdci 4399 nnsucelr 4428 nndisjeq 4429 leltfintr 4458 nnpw1ex 4484 tfinpw1 4494 tfinltfinlem1 4500 tfinltfin 4501 sfin112 4529 sfindbl 4530 sfinltfin 4535 vfinncvntnn 4548 nenpw1pwlem2 6085 ncspw1eu 6159 letc 6231 ce2le 6233 |
Copyright terms: Public domain | W3C validator |