![]() |
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 7 |
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 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: imbi12i 238 ancomsimp 1384 sbrim 1890 sbal1yz 1937 sbmo 2019 mo4f 2020 moanim 2034 necon4addc 2337 necon1bddc 2344 nfraldya 2428 r3al 2436 r19.23t 2498 ceqsralt 2668 ralab 2797 ralrab 2798 euind 2824 reu2 2825 rmo4 2830 rmo3f 2834 rmo4f 2835 reuind 2842 rmo3 2952 dfdif3 3133 raldifb 3163 unss 3197 ralunb 3204 inssdif0im 3377 ssundifim 3393 raaan 3416 pwss 3473 ralsnsg 3508 ralsns 3509 disjsn 3532 snss 3596 unissb 3713 intun 3749 intpr 3750 dfiin2g 3793 dftr2 3968 repizf2lem 4025 axpweq 4035 zfpow 4039 axpow2 4040 zfun 4294 uniex2 4296 setindel 4391 setind 4392 elirr 4394 en2lp 4407 zfregfr 4426 tfi 4434 raliunxp 4618 dffun2 5069 dffun4 5070 dffun4f 5075 dffun7 5086 funcnveq 5122 fununi 5127 fiintim 6746 addnq0mo 7156 mulnq0mo 7157 addsrmo 7439 mulsrmo 7440 prime 9002 raluz2 9224 ralrp 9312 modfsummod 11066 isprm4 11593 bdcriota 12662 bj-uniex2 12695 bj-ssom 12719 |
Copyright terms: Public domain | W3C validator |