Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3exp1 | Structured version Visualization version Unicode version |
Description: Exportation from left triple conjunction. (Contributed by NM, 24-Feb-2005.) |
Ref | Expression |
---|---|
3exp1.1 |
Ref | Expression |
---|---|
3exp1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp1.1 | . . 3 | |
2 | 1 | ex 450 | . 2 |
3 | 2 | 3exp 1264 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 w3a 1037 |
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 197 df-an 386 df-3an 1039 |
This theorem is referenced by: ltmpi 9726 cshf1 13556 lcmfunsnlem 15354 mulginvcom 17565 symgfvne 17808 voliunlem3 23320 3cyclfrgrrn 27150 frgrregord013 27253 strlem3a 29111 hstrlem3a 29119 chirredlem1 29249 nn0prpwlem 32317 matunitlindflem1 33405 zerdivemp1x 33746 athgt 34742 paddasslem14 35119 paddidm 35127 tendospcanN 36312 jm2.26 37569 relexpxpmin 38009 0ellimcdiv 39881 |
Copyright terms: Public domain | W3C validator |