| 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 73 |
. 2
| |
| 2 | anim1i.1 |
. 2
| |
| 3 | 1, 2 | anim12i 360 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: sylanl2 510 sylanr2 512 anbi2i 538 biantrud 795 3anandis 1196 19.41 1448 sbimi 1537 equs45f 1569 eupickb 1836 2euexOLD 1845 2exeu 1850 2eu1 1853 r19.27av 2224 rcla42ev 2385 reu3 2444 pssn2lpOLD 2710 difrab 2868 ssiunOLD 3294 trssord 3675 ordnbtwn 3761 dfwe2OLD 3862 tfi 3937 find 3977 imainss 4331 dffun8OLD 4449 fof 4617 dff1o2OLD 4640 dff1o3OLD 4642 f1ocnv 4651 fv3 4690 fvelimab 4725 fvelimabOLD 4726 dff2 4789 dffo5 4794 dff1o6 4853 ssoprab2i 4937 ndmoprass 4981 ndmoprdistr 4982 tfrlem5 5123 omlimcl 5257 odi 5258 mapval2 5394 ixpf 5415 uniixp 5416 isfinite1 5624 infcntss 5646 isfinite 5741 nnsdom 5742 zfregs 5754 aceq6b 5904 ac6 5917 ac6s 5918 zorn 5959 ondomon 6008 cflim 6057 axregndlem1 6106 axregnd 6108 halfpq 6234 ltexprlem1 6294 ltexprlem4 6297 prlem936a 6305 reclem3pr 6310 recexsrlem 6364 suppsr3 6376 pre-axsup 6444 divadddiv 6960 lediv2a 7080 lbreu 7254 supxr 7290 dfuzi 7414 fzrev2i 7691 shftf 7764 seqzp1 7791 bcval2 8211 clm4lei 8341 climaddc1 8378 climsub 8390 climcmplem 8397 isummulc1iALT 8474 infxpidmlem11 8831 infxpidmlem12 8832 subtop 8916 islp2 9023 cnpco 9046 cncnp 9055 sncld 9064 blfval 9112 blssex 9131 iscms2 9272 bcthlem7 9283 isgrp 9321 gxsub 9399 isga2 9452 gapmlem 9461 vcz 9521 sspival 9736 ubthlem10 9881 spweu 10000 grothpw 10134 grothpwex 10135 grothomex 10136 indexfi 10174 isflimf 10323 rngmgmbs4 10401 hvsub4 10538 hvaddsub4 10578 chsscmi 10745 chcmhi 10746 chocunii 10805 homcl 11157 osumlem5 11217 5oalem2 11235 5oalem5 11238 5oalem6 11239 3oalem2 11243 hoadddi 11366 lnopconi 11600 lnfnconi 11627 stle0i 11811 spansncv2 11865 mdsymlem1 11975 cdj3lem1 12006 bnj44OLD 12420 bnj143 12475 bnj168 12496 bnj512 12519 bnj1064 12900 bnj1167 12959 bnj518 13260 bnj546 13272 bnj583 13296 bnj594 13300 bnj1097 13412 bnj1100 13414 bnj1174 13442 dvdsnegb 13672 ndvdssub 13710 ordsucuniel 13863 lukshef-ax2 14239 dff1o6f 14416 isfinite1b 14434 sallnei 14873 cntrsetlem 14999 iintlem1 15010 trnij 15015 cptarc 15242 finminlem 15367 alexsublem3 15439 reconn 15451 ivthALT 15454 topfneec 15501 neibastop2lem3 15521 limfilcf 15587 flimfcls 15613 difxp 15690 indexa 15753 indexfiOLD 15755 frminex 15773 elfzp12 15795 totbndbnd 15944 rrntotbnd 16022 phtpycolem3 16053 phtpycolem4 16054 pcoloopf 16079 strss 16711 linepsub 17232 pmapsub 17250 elpaddri 17263 |
| 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 |