Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > bibi2i | Structured version Visualization version Unicode version |
Description: Inference adding a biconditional to the left in an equivalence. (Contributed by NM, 26-May-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 16-May-2013.) |
Ref | Expression |
---|---|
bibi2i.1 |
Ref | Expression |
---|---|
bibi2i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . . 3 | |
2 | bibi2i.1 | . . 3 | |
3 | 1, 2 | syl6bb 276 | . 2 |
4 | id 22 | . . 3 | |
5 | 4, 2 | syl6bbr 278 | . 2 |
6 | 3, 5 | impbii 199 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 196 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 |
This theorem is referenced by: bibi1i 328 bibi12i 329 bibi2d 332 con2bi 343 pm4.71r 663 xorass 1468 sblbis 2404 sbrbif 2406 abeq2 2732 abeq2f 2792 pm13.183 3344 symdifass 3853 disj3 4021 euabsn2 4260 axrep5 4776 axsep 4780 ax6vsep 4785 inex1 4799 axpr 4905 zfpair2 4907 sucel 5798 suppvalbr 7299 bnj89 30787 bnj145OLD 30795 axrepprim 31579 brtxpsd3 32003 bisym1 32418 bj-abeq2 32773 bj-axrep5 32792 bj-axsep 32793 bj-snsetex 32951 ifpidg 37836 nanorxor 38504 |
Copyright terms: Public domain | W3C validator |