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 1176 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 w3a 963 |
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 965 |
This theorem is referenced by: mob 2894 eqreu 2904 funimaexglem 5253 ssimaexg 5530 rbropap 6190 dfsmo2 6234 3ecoptocl 6569 distrnq0 7379 addassnq0 7382 uzind 9275 fzind 9279 fnn0ind 9280 xltnegi 9739 facwordi 10614 shftvalg 10736 shftval4g 10737 mulgcd 11900 coprmdvds1 11968 inopn 12412 basis1 12456 cnmpt2t 12704 cnmpt22 12705 cnmptcom 12709 xmeteq0 12770 sincosq1sgn 13158 sincosq2sgn 13159 sincosq3sgn 13160 sincosq4sgn 13161 speano5 13530 |
Copyright terms: Public domain | W3C validator |