| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Exportation from triple conjunction. |
| Ref | Expression |
|---|---|
| 3exp.1 |
|
| Ref | Expression |
|---|---|
| 3expib |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 3exp.1 |
. . 3
| |
| 2 | 1 | 3exp 844 |
. 2
|
| 3 | 2 | imp3a 368 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: vtocl3ga 1901 3ecoptocl 4366 fodomfib 4627 icoshf 6434 ser1add2i 6597 iserzmulc1 7226 mulc1cncf 7369 ivthlem6 7376 ivthlem7 7377 mettri4 7899 opnin 7954 opntop 7955 tgbl 7956 blbas 7957 grpdivf 8169 ghgrpi 8221 ipf 8450 sspival 8481 spwmo 8740 spwval 8743 pilem1 8754 sincosq1sgn 8787 sincosq2sgn 8788 sincosq3sgn 8789 sincosq4sgn 8790 efifolem4 8808 efifolem5 8809 shintcli 9376 adjadj 9943 unopadj2 9945 hmopadj 9946 ghomf1olem 10481 homcard 10633 qusp 10649 neifil 10661 filintf 10662 mrdmcd 10804 cmpassoh 10811 imonclem 10823 ismonc 10824 cmpmon 10825 icmpmon 10826 iepiclem 10833 isepic 10834 idfisf 10844 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 |
| This theorem depends on definitions: df-bi 154 df-an 232 df-3an 789 |