New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > 3impia | Unicode version |
Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) |
Ref | Expression |
---|---|
3impia.1 |
Ref | Expression |
---|---|
3impia |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3impia.1 | . . 3 | |
2 | 1 | ex 423 | . 2 |
3 | 2 | 3imp 1145 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 358 w3a 934 |
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 df-3an 936 |
This theorem is referenced by: mopick2 2271 3gencl 2889 mob2 3016 moi 3019 reupick3 3540 disjne 3596 tfindi 4496 sfin112 4529 sfinltfin 4535 vfintle 4546 fvun1 5379 ovmpt4g 5710 ov2gf 5711 letc 6230 nclenn 6248 nchoicelem9 6295 nchoicelem17 6303 frecxp 6312 |
Copyright terms: Public domain | W3C validator |