| 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 616 |
. 2
|
| 3 | ancom 435 |
. 2
| |
| 4 | ancom 435 |
. 2
| |
| 5 | 2, 3, 4 | 3bitr4g 555 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: bibi2d 618 anbi1 621 anbi12d 628 bi2anan9 632 pm5.71 748 drsb1 1175 sb7f 1341 eleq1 1534 rexeq1f 1784 reueq1f 1785 rabeqf 1808 eqvinc 1883 alexeq 1885 ceqex 1886 moi 1925 sbc3ang 1979 psstr 2150 difeq1 2153 ineq1 2210 r19.28zv 2350 ifeq1 2364 ifeq2 2365 prssg 2472 eluni 2506 csbopabg 2678 axrep1 2694 axrep2 2695 axrep3 2696 zfrepclf 2699 axsep 2702 axsep2 2704 zfauscl 2705 opthgg 2789 otthg 2790 copsexg 2792 copsex4g 2794 elopab 2811 opelopab2 2819 pocl 2844 uniuni 2880 rabxfr 2902 ordtri4 2984 dflim2 3025 limuni3 3123 xpeq1 3200 vtoclr 3211 opelxp 3214 opbrop 3238 coeq2 3282 opelco 3288 opelcog 3290 opelresg 3374 resopab2 3398 elxp4 3453 elxp5 3454 fun11 3562 feq2 3621 f1eq2 3661 f1eq3 3662 foeq2 3669 ssimaexg 3769 dmfco 3773 fvco 3774 isoeq5 3891 isoini 3900 f1oiso 3904 tz7.44-1 3928 rdglem2 3938 eloprabg 4007 resoprab 4009 oprabval 4023 oprabvalig 4024 oprabval2gf 4026 oprabval3 4030 oprabval6g 4032 2ndconst 4097 oarec 4196 ertr 4274 brecop 4306 ecopoprtrn 4311 th3qlem2 4315 th3q 4317 dom2d 4404 xpsnen 4435 xpassen 4441 pw2en 4446 mapxpen 4495 unfilem3 4550 unifiOLD 4557 preleq 4603 axinf 4623 r1pwcl 4687 aceq1 4729 aceq0 4730 aceq6a 4741 axac 4745 brdom7disj 4804 brdom6disj 4805 unxpdom 4844 cardcf 4911 cfeq0 4914 cfsuc 4915 axrepnd 4946 axunndlem1 4947 axinfnd 4958 axacndlem5 4963 axacnd 4964 zfcndrep 4966 zfcndinf 4970 zfcndac 4971 ltsopq 5075 ltrpq 5085 genpass 5112 distrlem1pr 5127 distrlem5pr 5131 ltprord 5134 reclem2pr 5157 reclem3pr 5158 recexpr 5160 ltsosr 5203 mulgt0sr 5214 ltresr 5258 ltsor 5261 pre-axmulgt0 5290 ltxrt 5495 lt2addt 5643 le2addt 5644 addgt0t 5647 addgegt0t 5648 addge0t 5650 mulge0t 5679 ltrect 5884 lerect 5885 lt2msqt 5886 le2msqt 5903 supxr2 6082 supxrre 6083 primet 6195 peano5uzt 6204 uzindOLD 6208 qbtwnre 6278 qbtwnxr 6279 ioovalt 6366 iocvalt 6375 icovalt 6376 iccvalt 6377 icoun 6413 snunioolem 6414 rexuz 6444 fzvalt 6469 sq11t 6629 nn0opth2t 6668 sqrlem12 6684 sqrlet 6713 sqr00t 6714 sqr2irrlem2 6725 crut 6738 lenegsqt 6885 abs2difabst 6903 abs3lemt 6907 cau3i 6914 cau3ir 6915 sumeq1 6982 dffsum 6998 fsumsplit 7020 climfnn 7092 climunii 7098 climuni 7099 dfisum 7191 cncfval 7264 znnenlem 7501 basis2t 7615 tg2t 7621 tgval3t 7625 tgss2t 7637 neival 7717 isneip 7720 qdensere 7751 iscn 7758 cnpval 7759 iscnp 7760 blfval 7835 opni 7864 opnin 7869 neibl 7877 metcnp 7887 metcn 7889 cncfmet 7905 lmfval 7925 iscau 7936 bcthlem15 8013 isgrp2i 8076 vci 8167 isvclem 8196 ipfval 8352 nmofval 8425 isph 8481 spwval2 8653 pilem1 8671 sincosq2sgn 8705 sincosq4sgn 8707 efifolem3 8724 norm3lemt 9019 hlim 9056 hlim2 9060 closedsub 9093 hlimunii 9108 hlimuni 9109 occllem8 9180 projlem1 9186 projlem7 9192 projlem20 9205 shlubt 9354 cmbrt 9527 eigret 9761 eigortht 9764 cvbrt 10209 mdbrt 10221 dmdbrt 10226 chrelat2t 10297 mdsymlem2 10331 elo 10444 subsp 10554 qusp 10555 cnfilca 10583 cnfilcaOLD 10584 isalg 10653 eloi 10659 algi 10660 isded 10669 dedi 10670 iscat 10687 cati 10688 cmpasso 10706 isfuna 10754 |
| 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 147 df-an 225 |