![]() |
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 236 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | ax-mp 5 |
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: imbi12i 239 ancomsimp 1451 sbrim 1968 sbal1yz 2013 sbmo 2097 mo4f 2098 moanim 2112 necon4addc 2430 necon1bddc 2437 nfraldya 2525 r3al 2534 r19.23t 2597 ceqsralt 2779 ralab 2912 ralrab 2913 euind 2939 reu2 2940 rmo4 2945 rmo3f 2949 rmo4f 2950 reuind 2957 rmo3 3069 dfdif3 3260 raldifb 3290 unss 3324 ralunb 3331 inssdif0im 3505 ssundifim 3521 raaan 3544 pwss 3609 ralsnsg 3647 ralsns 3648 disjsn 3672 snssOLD 3736 snssb 3743 unissb 3857 intun 3893 intpr 3894 dfiin2g 3937 dftr2 4121 repizf2lem 4182 axpweq 4192 zfpow 4196 axpow2 4197 zfun 4455 uniex2 4457 setindel 4558 setind 4559 elirr 4561 en2lp 4574 zfregfr 4594 tfi 4602 raliunxp 4789 dffun2 5248 dffun4 5249 dffun4f 5254 dffun7 5265 funcnveq 5301 fununi 5306 pw1dc0el 6943 fiintim 6961 addnq0mo 7481 mulnq0mo 7482 addsrmo 7777 mulsrmo 7778 prime 9387 raluz2 9615 ralrp 9711 modfsummod 11507 nnwosdc 12081 isprm4 12162 dedekindicclemicc 14595 bdcriota 15121 bj-uniex2 15154 bj-ssom 15174 |
Copyright terms: Public domain | W3C validator |