Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > orbi2i | Unicode version |
Description: Inference adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Dec-2012.) |
Ref | Expression |
---|---|
orbi2i.1 |
Ref | Expression |
---|---|
orbi2i |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orbi2i.1 | . . . 4 | |
2 | 1 | biimpi 113 | . . 3 |
3 | 2 | orim2i 678 | . 2 |
4 | 1 | biimpri 124 | . . 3 |
5 | 4 | orim2i 678 | . 2 |
6 | 3, 5 | impbii 117 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 98 wo 629 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 630 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: orbi1i 680 orbi12i 681 orass 684 or4 688 or42 689 orordir 691 testbitestn 823 orbididc 860 3orcomb 894 excxor 1269 xordc 1283 nf4dc 1560 nf4r 1561 19.44 1572 dveeq2 1696 dvelimALT 1886 dvelimfv 1887 dvelimor 1894 dcne 2216 unass 3100 undi 3185 undif3ss 3198 symdifxor 3203 undif4 3284 iinuniss 3737 ordsucim 4226 suc11g 4281 qfto 4714 nntri3or 6072 reapcotr 7589 elnn0 8183 elnn1uz2 8544 nn01to3 8552 elxr 8696 bj-peano4 10080 |
Copyright terms: Public domain | W3C validator |