New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > bibi2i | Unicode version |
Description: Inference adding a biconditional to the left in an equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 16-May-2013.) |
Ref | Expression |
---|---|
bibi.a |
Ref | Expression |
---|---|
bibi2i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 19 | . . 3 | |
2 | bibi.a | . . 3 | |
3 | 1, 2 | syl6bb 252 | . 2 |
4 | id 19 | . . 3 | |
5 | 4, 2 | syl6bbr 254 | . 2 |
6 | 3, 5 | impbii 180 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 176 |
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 177 |
This theorem is referenced by: bibi1i 305 bibi12i 306 bibi2d 309 con2bi 318 pm4.71r 612 xorass 1308 sblbis 2072 sbrbif 2074 abeq2 2458 abid2f 2514 pm13.183 2979 dfss2 3262 necompl 3544 disj3 3595 euabsn2 3791 axprimlem1 4088 axprimlem2 4089 axxpprim 4090 axsiprim 4093 axtyplowerprim 4094 axins2prim 4095 axins3prim 4096 ninexg 4097 1cex 4142 eqpw1 4162 xpkvexg 4285 p6exg 4290 eqop 4611 |
Copyright terms: Public domain | W3C validator |