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 179 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: imbi12i 238 anidmdbi 395 nan 666 sbcof2 1766 sblimv 1850 sbhb 1893 sblim 1908 2sb6 1937 sbcom2v 1938 2sb6rf 1943 eu1 2002 moabs 2026 mo3h 2030 moanim 2051 2moswapdc 2067 r2alf 2429 r19.21t 2484 rspc2gv 2775 reu2 2845 reu8 2853 2reuswapdc 2861 2rmorex 2863 dfdif3 3156 ssconb 3179 ssin 3268 reldisj 3384 ssundifim 3416 ralm 3437 unissb 3736 repizf2lem 4055 elirr 4426 en2lp 4439 tfi 4466 ssrel 4597 ssrel2 4599 fncnv 5159 fun11 5160 axcaucvglemres 7675 axpre-suploc 7678 suprzclex 9117 raluz2 9342 supinfneg 9358 infsupneg 9359 infssuzex 11569 bezoutlemmain 11613 isprm2 11725 lmres 12344 limcdifap 12727 |
Copyright terms: Public domain | W3C validator |