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 750 | . 2 |
4 | 1 | biimpri 132 | . . 3 |
5 | 4 | orim2i 750 | . 2 |
6 | 3, 5 | impbii 125 | 1 |
Colors of variables: wff set class |
Syntax hints: wb 104 wo 697 |
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 698 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: orbi1i 752 orbi12i 753 orass 756 or4 760 or42 761 orordir 763 dcnnOLD 834 orbididc 937 3orcomb 971 excxor 1356 xordc 1370 nf4dc 1648 nf4r 1649 19.44 1660 dveeq2 1787 dvelimALT 1983 dvelimfv 1984 dvelimor 1991 dcne 2317 unass 3228 undi 3319 undif3ss 3332 symdifxor 3337 undif4 3420 iinuniss 3890 ordsucim 4411 suc11g 4467 qfto 4923 nntri3or 6382 reapcotr 8353 elnn0 8972 elxnn0 9035 elnn1uz2 9394 nn01to3 9402 elxr 9556 xaddcom 9637 xnegdi 9644 xpncan 9647 xleadd1a 9649 lcmdvds 11749 mulgcddvds 11764 cncongr2 11774 bj-peano4 13142 |
Copyright terms: Public domain | W3C validator |