Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > imbi1i | Unicode version |
Description: Introduce a consequent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.) |
Ref | Expression |
---|---|
imbi1i.1 |
Ref | Expression |
---|---|
imbi1i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imbi1i.1 | . 2 | |
2 | imbi1 235 | . 2 | |
3 | 1, 2 | ax-mp 5 | 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 ancomsimp 1401 sbrim 1907 sbal1yz 1954 sbmo 2036 mo4f 2037 moanim 2051 necon4addc 2355 necon1bddc 2362 nfraldya 2446 r3al 2454 r19.23t 2516 ceqsralt 2687 ralab 2817 ralrab 2818 euind 2844 reu2 2845 rmo4 2850 rmo3f 2854 rmo4f 2855 reuind 2862 rmo3 2972 dfdif3 3156 raldifb 3186 unss 3220 ralunb 3227 inssdif0im 3400 ssundifim 3416 raaan 3439 pwss 3496 ralsnsg 3531 ralsns 3532 disjsn 3555 snss 3619 unissb 3736 intun 3772 intpr 3773 dfiin2g 3816 dftr2 3998 repizf2lem 4055 axpweq 4065 zfpow 4069 axpow2 4070 zfun 4326 uniex2 4328 setindel 4423 setind 4424 elirr 4426 en2lp 4439 zfregfr 4458 tfi 4466 raliunxp 4650 dffun2 5103 dffun4 5104 dffun4f 5109 dffun7 5120 funcnveq 5156 fununi 5161 fiintim 6785 addnq0mo 7223 mulnq0mo 7224 addsrmo 7519 mulsrmo 7520 prime 9118 raluz2 9342 ralrp 9431 modfsummod 11195 isprm4 11727 dedekindicclemicc 12706 bdcriota 13008 bj-uniex2 13041 bj-ssom 13061 |
Copyright terms: Public domain | W3C validator |