![]() |
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 265 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | id 22 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4, 2 | syl6bbr 267 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | impbii 191 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() |
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 189 |
This theorem is referenced by: bibi1i 316 bibi12i 317 bibi2d 320 con2bi 330 pm4.71r 637 xorass 1409 xorassOLD 1410 sblbis 2233 sbrbif 2235 abeq2 2560 abeq2f 2619 pm13.183 3179 symdifass 3672 disj3 3809 euabsn2 4043 axrep5 4520 axsep 4524 ax6vsep 4529 inex1 4544 axpr 4638 zfpair2 4640 sucel 5496 suppvalbr 6918 bnj89 29527 bnj145OLD 29535 axrepprim 30329 brtxpsd3 30663 bisym1 31079 bj-abeq2 31388 bj-axrep5 31407 bj-axsep 31408 bj-snsetex 31557 ifpidg 36135 nanorxor 36653 |
Copyright terms: Public domain | W3C validator |