| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Deduction adding a consequent to both sides of a logical equivalence. |
| Ref | Expression |
|---|---|
| bid.1 |
|
| Ref | Expression |
|---|---|
| imbi1d |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | bid.1 |
. . . 4
| |
| 2 | 1 | negbid 609 |
. . 3
|
| 3 | 2 | imbi2d 610 |
. 2
|
| 4 | pm4.1 164 |
. 2
| |
| 5 | pm4.1 164 |
. 2
| |
| 6 | 3, 4, 5 | 3bitr4g 553 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: bibi2d 616 imbi1 621 imbi12d 624 pm5.33 648 con3th 764 drsb1 1171 ax11v2 1210 ax11inda 1364 rgen2a 1691 ralcom2 1768 raleq1f 1775 alexeq 1876 mo2icl 1914 sbcth2 1972 sbc19.21g 1977 ra4sbc 1987 r19.37zv 2341 ssuni 2512 intmin4 2549 trel 2677 ssexg 2711 dtruALT 2738 opth2 2789 pocl 2835 so 2855 onminex 3010 ordunisuc2 3105 dfom2 3123 findsg 3147 tfindsg 3152 tfindsg2 3153 vtoclr 3201 fun11 3548 funimass4 3748 f1fv 3859 caoprcan 4041 oaabs 4236 ertr 4258 ecoptocl 4287 ecopoprtrn 4295 dom2d 4385 unifi 4532 fiint 4534 supmo 4550 supub 4554 suplub 4555 suppr 4562 supsnALT 4564 karden 4698 aceq1 4701 zorn2lem1 4760 iscard2 4826 axrepndlem2 4917 axregndlem2 4927 indpi 5006 ltsopq 5047 prcdpq 5069 prlem934 5111 supexpr 5135 ltsosr 5175 suppsr 5194 supsrlem6 5202 supsr 5203 supre 5232 ltsor 5233 prodgt0 5775 prodgt0t 5782 prodge0t 5784 lbinfm 5995 infm3 6001 infmsup 6015 xrsupsslem 6023 xrinfmsslem 6024 supxr 6028 primet 6142 raluz 6374 fz1sbct 6449 sqrlem20 6622 abs3lemt 6844 seq1bnd 6847 cau2 6850 cau3i 6851 cau3ir 6852 cau5i 6854 cvg1 6858 cvg3 6860 cvganz 6861 clm3 7017 clm4 7018 climconst 7031 climshft 7041 climaddlem3 7052 climmullem8 7063 caucvglem2 7094 caucvglem5 7097 serzf0 7105 ser1f0 7106 ser1clim0 7109 cvgcmp3cetlem2 7125 cvgcmp3cet 7126 expcnvlem1 7162 expcnvlem6 7167 elcncf1d 7205 ivthlem6 7221 ivthlem7 7222 ivthlem6OLD 7230 ivthlem7OLD 7231 efaddlem25 7304 islp2 7688 cncnplem3 7715 metcnpi3 7831 metcnpi4 7832 metcni2 7834 cncfmet 7844 lmconst 7872 lmnn 7873 caun0 7880 metcld 7901 metcnp4 7904 xplm 7909 xpcn 7910 iscms2lem4 7926 isnvlem 8167 isnvgOLD 8168 nvi 8173 nmcnilem 8272 va1cnlem 8279 sm1cnilem 8281 blocni 8396 spwval2 8577 efifolem3 8639 norm3lemt 8940 chlim 9025 hlim0 9026 projlem20 9121 pjth 9148 omlsi 9160 eigortht 9681 0cnop 9819 0cnfn 9820 idcnop 9821 lnopcon 9878 lnfncon 9905 nlelch 9909 stcltr1 10111 elat2 10175 ghomf1olem 10301 fillsb 10435 isded 10513 dedi 10514 iscat 10531 cati 10532 ismona 10579 ismonb 10580 imonclem 10583 |
| 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 |