![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > imbi2i | Unicode version |
Description: Introduce an antecedent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 6-Feb-2013.) |
Ref | Expression |
---|---|
bi.a |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
imbi2i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bi.a |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | a1i 9 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | pm5.74i 169 |
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: imbi12i 228 anidmdbi 378 nan 625 sbcof2 1688 sblimv 1771 sbhb 1813 sblim 1828 2sb6 1857 sbcom2v 1858 2sb6rf 1863 eu1 1922 moabs 1946 mo3h 1950 moanim 1971 2moswapdc 1987 r2alf 2335 r19.21t 2388 reu2 2723 reu8 2731 2reuswapdc 2737 2rmorex 2739 ssconb 3070 ssin 3153 reldisj 3265 ssundifim 3300 ralm 3319 unissb 3601 repizf2lem 3905 elirr 4224 en2lp 4232 tfi 4248 ssrel 4371 ssrel2 4373 fncnv 4908 fun11 4909 raluz2 8298 |
Copyright terms: Public domain | W3C validator |