| 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 1066 |
. 2
|
| 3 | 2 | imp3a 388 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: vtocl3ga 2354 fco 4573 fvco2 4737 onfununi 5116 3ecoptocl 5364 fodomfib 5657 icoshft 7577 fzen 7664 ser1add2i 7751 iserzmulc1 8396 mulc1cncf 8541 ivthlem6 8548 ivthlem7 8549 mettri4 9091 opnin 9146 opntop 9147 tgbl 9148 blbas 9149 grpdivf 9370 ipf 9705 sspival 9736 spwmo 9999 spwval 10002 pilem1 10020 sincosq1sgn 10053 sincosq2sgn 10054 sincosq3sgn 10055 sincosq4sgn 10056 efifolem4 10079 efifolem5 10080 hausnei2 10222 filintf 10274 filfbas 10276 fsubbas 10281 neifil 10302 hausfillim 10303 flimopn 10321 shintcli 10926 adjadj 11497 unopadj2 11499 hmopadj 11500 bnj1200 12977 bnj1381 13098 bnj594 13300 bnj580 13301 bnj600 13308 bnj1321 13498 bnj1367 13511 ghomf1olem 13637 algcvga 13747 dvdsgcd 13765 cur1vald 14547 curgrpact 14735 addvecom 14809 invaddvec 14810 svli2 14826 truni2 14850 inttop2 14863 homcard 14893 qusp 14908 conttnf 14944 bsi2 14992 intrn 14994 lvsovso 15038 dualcat2lem 15129 dualded 15132 dualcat2 15133 mrdmcd 15143 cmpassoh 15150 imonclem 15162 ismonc 15163 cmpmon 15164 icmpmon 15165 iepiclem 15172 isepic 15173 idfisf 15189 isline1 15294 elfiun 15369 fitop 15401 fness 15491 locfincomp 15514 topmtcl 15525 ist1-2 15542 ist1-3 15543 filssufillem 15570 filcon 15580 fmfnfmlem4 15597 filnetlem4 15643 neificl 15841 metf1o 15843 haustlmu 15906 heiborlem29 15983 rrnmet 16016 abl4pnp 16037 divrngcl 16110 keridl 16180 prnc 16215 linepsub 17232 pmapsub 17250 |
| 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 164 df-an 242 df-3an 860 |