| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Introduce conjunct to both sides of an implication. |
| Ref | Expression |
|---|---|
| anim1i.1 |
|
| Ref | Expression |
|---|---|
| anim2i |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id 59 |
. 2
| |
| 2 | anim1i.1 |
. 2
| |
| 3 | 1, 2 | anim12i 340 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: sylanl2 472 sylanr2 474 anbi2i 491 biantrud 738 3anandis 932 sbimi 1215 equs45f 1242 eupickb 1478 2euex 1484 2exeu 1489 2eu1 1492 rcla42ev 1928 reu6 1979 pssn2lp 2198 difrab 2324 ssiun 2646 dfwe2 2992 trssord 3022 ordnbtwn 3120 tfi 3183 find 3212 imainss 3520 dffun7 3597 fof 3729 f1o2 3750 f1o3 3751 fv3 3790 fvelimab 3822 dff4 3873 dffo5 3878 f1ofv 3935 tfrlem5 3973 ssoprab2i 4066 ndmoprass 4106 ndmoprdistr 4107 omlimcl 4267 odi 4268 mapval2 4396 ixpf 4417 uniixp 4418 isfinite1 4595 infcntss 4616 isfinite 4696 nnsdom 4697 zfregs 4709 aceq6b 4804 ac6 4817 ac6s 4818 zorn 4859 ondomon 4921 cflim 4974 axregndlem1 5019 axregnd 5021 halfpq 5147 ltexprlem1 5207 ltexprlem4 5210 prlem936a 5218 reclem3pr 5223 recexsrlem 5277 suppsr3 5289 pre-axsup 5356 divcan5 5839 divdivdiv 5843 divdivmul 5853 lediv2a 5957 nndivtr 6021 lbreu 6127 supxr 6163 dfuzi 6287 fzrev2i 6539 shftf 6610 seqzp1 6637 bcval2 7049 clm4lei 7171 climaddc1 7208 climsub 7220 climcmplem 7227 isummulc1iALT 7303 efsub 7461 infxpidmlem11 7654 infxpidmlem12 7655 subtop 7733 islp2 7832 cnpco 7854 cncnp 7863 sncld 7872 blfval 7920 blssex 7939 iscms2 8079 bcthlem7 8090 isgrp 8126 vcz 8273 sspival 8481 ubthlem10 8622 spweu 8741 grothinf 8864 hvsub4 8989 hvaddsub4 9028 chsscmi 9195 chcmhi 9196 chocunii 9255 homcl 9607 osumlem5 9665 5oalem2 9683 5oalem5 9686 5oalem6 9687 3oalem2 9691 hoadddi 9812 lnopconi 10046 lnfnconi 10073 stle0i 10250 spansncv2 10304 mdsymlem1 10414 cdj3lem1 10445 iintlem1 10714 trnij 10719 |
| 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 |