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 119 | . . 3 |
3 | 2 | orim2i 735 | . 2 |
4 | 1 | biimpri 132 | . . 3 |
5 | 4 | orim2i 735 | . 2 |
6 | 3, 5 | impbii 125 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wo 682 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 683 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: orbi1i 737 orbi12i 738 orass 741 or4 745 or42 746 orordir 748 dcnnOLD 819 orbididc 922 3orcomb 956 excxor 1341 xordc 1355 nf4dc 1633 nf4r 1634 19.44 1645 dveeq2 1771 dvelimALT 1963 dvelimfv 1964 dvelimor 1971 dcne 2296 unass 3203 undi 3294 undif3ss 3307 symdifxor 3312 undif4 3395 iinuniss 3865 ordsucim 4386 suc11g 4442 qfto 4898 nntri3or 6357 reapcotr 8328 elnn0 8947 elxnn0 9010 elnn1uz2 9369 nn01to3 9377 elxr 9531 xaddcom 9612 xnegdi 9619 xpncan 9622 xleadd1a 9624 lcmdvds 11687 mulgcddvds 11702 cncongr2 11712 bj-peano4 13080 |
Copyright terms: Public domain | W3C validator |