![]() |
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 | bitrdi 196 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | id 19 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4, 2 | bitr4di 198 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | impbii 126 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: bibi1i 228 bibi12i 229 bibi2d 232 pm4.71r 390 sblbis 1976 sbrbif 1978 abeq2 2302 abid2f 2362 necon4biddc 2439 pm13.183 2898 disj3 3499 euabsn2 3687 a9evsep 4151 inex1 4163 zfpair2 4239 sucel 4441 bdinex1 15391 bj-zfpair2 15402 bj-d0clsepcl 15417 |
Copyright terms: Public domain | W3C validator |