| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Deduction adding a right conjunct to both sides of a logical equivalence. |
| Ref | Expression |
|---|---|
| bid.1 |
|
| Ref | Expression |
|---|---|
| anbi1d |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bid.1 |
. . 3
| |
| 2 | 1 | anbi2d 751 |
. 2
|
| 3 | ancom 414 |
. 2
| |
| 4 | ancom 414 |
. 2
| |
| 5 | 2, 3, 4 | 3bitr4g 745 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: bibi2d 753 anbi1 756 anbi12d 763 bi2anan9 950 pm5.71 1061 drsb1 1819 eleq1 2204 rexeqf 2509 reueq1f 2510 rabeqf 2534 alexeq 2630 ceqex 2631 moi 2681 sbc5g 2712 rmoi 2772 psstr 2936 ineq1 3002 difin2 3064 r19.28z 3161 r19.28zv 3164 ifeq1 3183 eluni 3369 csbopabg 3577 axrep1 3597 axrep2 3598 axrep3 3599 zfrepclf 3602 axsep 3605 axsep2 3607 zfauscl 3608 opthgg 3697 otthg 3698 copsexg 3700 copsex4g 3703 elopab 3721 opelopab2 3730 pocl 3756 posn 3762 dflim2 3866 uniuni 3944 eusv2OLD 3963 eusv2 3964 reusv2lem4 3970 rabxfrd 3988 limuni3 4073 xpeq1 4149 vtoclr 4167 opbrop 4197 opelco 4259 opelco2g 4261 opelresg 4347 resopab2 4376 elxp4 4482 elxp5 4483 fun11 4581 feq2 4648 f1eq2 4693 f1eq3 4694 foeq2 4702 ssimaexg 4815 dmfco 4821 fvco 4822 respreima 4872 opabex3 4933 isoeq5 4962 isoini 4973 f1oiso 4977 f1oiso2 4978 oprabid 5002 eloprabg 5029 resoprab 5031 oprabval 5045 oprabvalig 5046 oprabval2gf 5049 oprabval3 5053 oprabval6g 5056 oprabopabf 5170 fparlem3 5206 fparlem4 5207 frxp 5210 xporderlem 5211 poxp 5212 fnwelem 5215 smoel2 5274 tz7.44-1 5300 rdglem2 5310 oarec 5407 omeu 5426 ertr 5492 brecop 5526 ecopoprtrn 5531 th3qlem2 5535 th3q 5537 dom2d 5624 xpsnen 5658 xpassen 5664 pw2en 5671 riotaeqdv 5730 xpen 5767 xpeng 5769 xpengOLDOLD 5770 mapen 5774 mapxpen 5780 unxpdom 5820 xpfir 5838 unfilem3 5862 unifi 5870 preleq 5940 zfinf 5962 r1pwcl 6034 r0weon 6146 aceq1 6183 aceq0 6184 aceq6a 6195 cdaeng 6245 cardcf 6271 cfeq0 6275 cfsuc 6276 cff1 6278 zfac 6315 brdom7disj 6380 brdom6disj 6381 unxpdomOLD 6411 cfeq0OLD 6446 cfsucOLD 6447 axrepnd 6464 axunndlem1 6465 axinfnd 6476 axacndlem5 6481 axacnd 6482 zfcndrep 6484 zfcndinf 6488 zfcndac 6489 ltsopq 6593 ltrpq 6603 genpass 6630 distrlem1pr 6645 distrlem5pr 6649 ltprord 6652 reclem2pr 6675 reclem3pr 6676 recexpr 6678 ltsosr 6721 mulgt0sr 6732 ltresr 6776 ltsor 6779 pre-axmulgt0 6806 ltxr 6854 lt2add 7165 le2add 7166 mulge0 7201 mulge0OLD 7202 ltrec 7400 lerec 7401 lt2msq 7402 le2msq 7419 supxr2 7631 supxrre 7632 prime 7750 peano5uzti 7759 uzindOLD 7763 qbtwnre 7805 qbtwnxr 7806 iooval 7879 iocval 7888 icoval 7889 iccval 7890 icoun 7928 snunioolem 7929 rexuz 7960 fzval 8000 sq11 8258 nn0opth2 8302 sqrlem12 8318 sqrle 8347 sqr00 8348 sqr2irrlem2 8359 cru 8372 lenegsq 8521 abs2difabs 8540 abs3lem 8544 cau3ii 8551 cau3iri 8552 sumeq1 8638 dffsum 8654 fsumsplit 8676 climfnn 8748 climunii 8754 climuni 8755 dfisum 8848 cncfval 8924 znnenlem 9169 divalg2 9302 gcdval 9309 1arithlem30 9424 1arithlem31 9425 isgrp 9464 isring 9508 basis2 9735 tg2 9742 tgval3 9746 tgss2 9758 neival 9858 isneip 9861 qdensere 9893 iscn 9900 cnpval 9901 iscnp 9902 blfval 9978 opni 10007 opnin 10012 neibl 10020 metcnp 10031 metcn 10033 cncfmet 10049 lmfval 10069 iscau 10080 bcthlem15 10157 grp2grpo 10190 isgrp2i 10229 gxoprval 10249 gapmlem 10330 drngi 10362 vci 10368 isvclem 10397 ipfval 10560 nmofval 10633 isph 10691 spwval2 10867 pilem1 10891 sincosq2sgn 10925 sincosq4sgn 10927 efifolem3 10949 txcn 11062 2txcn 11064 subspi 11079 hausfillim 11141 filmapf 11145 flimff 11155 flimopn 11159 dirtr 11194 dirge 11195 norm3lemt 11488 hlimi 11525 hlim2 11529 closedsub 11560 hlimuniii 11575 hlimunii 11576 occllem8 11647 projlem1 11653 projlem7 11659 projlem20 11672 shlub 11821 cmbr 11992 eigre 12230 eigorth 12233 cvbr 12685 mdbr 12697 dmdbr 12702 chrelat2 12773 mdsymlem2 12807 bnj957 13623 bnj1146 13714 dfon2lem6 14488 dfon2lem7 14489 dfon2lem8 14490 dfon2 14492 omopth 14504 xporderlemOLD 14601 poxpOLD 14602 frxpOLD 14604 poseq 14607 soseq 14608 sltval 14654 axdenselem5 14692 nocvxminlem 14697 axfelem12 14710 axfelem18 14716 axfelem22 14720 alexeqd 15002 fnoprvpop 15046 dfoprab4spop 15047 elo 15050 eloi 15112 infsdomnng 15135 surjsec2 15179 ispr1 15235 isprj1 15244 cbicplem 15247 prjmapcp2 15254 iscst2 15259 islatalg 15270 cur1vald 15286 prodeq1 15397 dffprod 15409 fprodadd 15448 vecval1b 15547 vecval3b 15548 vri 15587 sallnei 15630 osneisi 15632 qusp 15671 cnfilca 15693 exopcopn 15721 topsinind 15745 istopgrp 15749 topgrpi 15750 trhom 15761 ltrhom 15766 lvsovso 15832 isalg 15862 algi 15868 isded 15877 dedi 15878 iscat 15895 cati 15896 cmpasso 15914 dualalg 15925 isfuna 15976 tarval2 16059 tarval2g 16060 vtarsuelt 16082 efp2 16100 isplibg2 16121 trer 16185 finminlem 16191 fictb 16195 cnsubsp2 16251 compfipin0 16260 reconnlem5 16274 ivthALT 16278 1stcclb 16295 2ndc1stc 16301 2ndcctbss 16302 isfne3 16306 fnessex 16308 comppfsc 16341 fnemeet1 16352 ist1-2 16366 ist1-3 16367 t1sep 16370 nrmsep2 16379 ufileu 16397 ufinffr 16402 ufilen 16403 cnpfillim 16413 fcluscf 16436 ufcomp 16446 tailf 16457 filnetlem1 16464 filnetlem2 16465 filnetlem3 16466 filnetlem4 16467 filnetlem5 16468 filnet 16469 cover2 16497 cover2g 16498 difin2OLD 16500 respreimaOLD 16508 xpengOLD 16515 opabex3OLD 16525 fvopabf4g 16527 oprabvalg 16530 resoprab2 16534 eropreu 16557 eroprv 16558 acdcg 16574 add20 16601 sdclem2 16634 sdc 16635 fdc 16636 fdc1 16637 blssp 16668 cnss 16716 lmtlm 16732 txcnoprab 16735 cnresoprab 16739 cnoprab1 16745 cnoprab2 16746 totbndss 16761 ismtyhmeolem 16774 heiborlem25 16803 heiborlem26 16804 heiborlem28 16806 heiborlem30 16808 phtpyfval 16870 phtpyval 16871 phtpcval 16882 isphtpc 16883 pcofval 16896 pcoval 16897 pi1bval 16912 isdivrng1 16933 isriscg 16962 iscringd 16971 isfldidl2 17041 ertr2 17081 2sbc6g 17203 2sbc5g 17204 iotasbc 17207 dropab1 17248 dropab2 17249 cvrval 17661 cvrnbtwn3 17667 iscvlat2 17721 ishlat3 17750 hlrelat5 17796 3dim0 17853 issrng 17888 islvec 17900 isphil 17907 llnexatOLD 17953 llnexat 17954 islpln5 17966 islvol5 18011 pointpsub 18183 pmapjat1 18285 ltrnu 18474 cdleme02 18591 |
| 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 220 df-an 339 |