![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE 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 185 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | id 19 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4, 2 | syl6bbr 187 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | impbii 117 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: bibi1i 217 bibi12i 218 bibi2d 221 pm4.71r 370 sblbis 1831 sbrbif 1833 abeq2 2143 abid2f 2199 necon4biddc 2274 pm13.183 2675 disj3 3266 euabsn2 3430 a9evsep 3870 inex1 3882 zfpair2 3936 sucel 4113 bdinex1 9354 bj-zfpair2 9365 bj-d0clsepcl 9384 |
Copyright terms: Public domain | W3C validator |