Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > imbi1d | Unicode version |
Description: Deduction adding 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 |
---|---|
imbid.1 |
Ref | Expression |
---|---|
imbi1d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | imbid.1 | . . . 4 | |
2 | 1 | biimprd 147 | . . 3 |
3 | 2 | imim1d 69 | . 2 |
4 | 1 | biimpd 132 | . . 3 |
5 | 4 | imim1d 69 | . 2 |
6 | 3, 5 | impbid 120 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 98 |
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: imbi12d 223 imbi1 225 imim21b 241 pm5.33 541 imordc 796 drsb1 1680 ax11v2 1701 ax11v 1708 ax11ev 1709 equs5or 1711 raleqf 2501 alexeq 2670 mo2icl 2720 sbc19.21g 2826 csbiebg 2889 ralss 3006 ssuni 3602 intmin4 3643 ssexg 3896 pocl 4040 frforeq1 4080 frforeq2 4082 frind 4089 ontr2exmid 4250 elirr 4266 en2lp 4278 tfisi 4310 vtoclr 4388 sosng 4413 fun11 4966 funimass4 5224 dff13 5407 f1mpt 5410 isopolem 5461 oprabid 5537 caovcan 5665 caoftrn 5736 dfsmo2 5902 qliftfun 6188 ecoptocl 6193 ecopovtrn 6203 ecopovtrng 6206 dom2lem 6252 ssfiexmid 6336 findcard 6345 findcard2 6346 findcard2s 6347 ltsonq 6496 prarloclem3 6595 lttrsr 6847 mulextsr1 6865 axpre-lttrn 6958 axpre-mulext 6962 axcaucvglemres 6973 prime 8337 raluz 8521 indstr 8536 fz1sbc 8958 qbtwnzlemshrink 9104 rebtwn2zlemshrink 9108 caucvgre 9580 addcn2 9831 mulcn2 9833 cn1lem 9834 sqrt2irr 9878 bj-rspgt 9925 bdssexg 10024 |
Copyright terms: Public domain | W3C validator |