Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3impib | Unicode version |
Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) |
Ref | Expression |
---|---|
3impib.1 |
Ref | Expression |
---|---|
3impib |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3impib.1 | . . 3 | |
2 | 1 | expd 256 | . 2 |
3 | 2 | 3imp 1175 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 962 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 964 |
This theorem is referenced by: mob 2861 eqreu 2871 funimaexglem 5201 ssimaexg 5476 rbropap 6133 dfsmo2 6177 3ecoptocl 6511 distrnq0 7260 addassnq0 7263 uzind 9155 fzind 9159 fnn0ind 9160 xltnegi 9611 facwordi 10479 shftvalg 10601 shftval4g 10602 mulgcd 11693 coprmdvds1 11761 inopn 12159 basis1 12203 cnmpt2t 12451 cnmpt22 12452 cnmptcom 12456 xmeteq0 12517 sincosq1sgn 12896 sincosq2sgn 12897 sincosq3sgn 12898 sincosq4sgn 12899 speano5 13131 |
Copyright terms: Public domain | W3C validator |