![]() |
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 751 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1 | biimpri 132 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | orim2i 751 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | impbii 125 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
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 699 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: orbi1i 753 orbi12i 754 orass 757 or4 761 or42 762 orordir 764 dcnnOLD 835 orbididc 938 3orcomb 972 excxor 1357 xordc 1371 nf4dc 1649 nf4r 1650 19.44 1661 dveeq2 1788 dvelimALT 1986 dvelimfv 1987 dvelimor 1994 dcne 2320 unass 3238 undi 3329 undif3ss 3342 symdifxor 3347 undif4 3430 iinuniss 3903 ordsucim 4424 suc11g 4480 qfto 4936 nntri3or 6397 reapcotr 8384 elnn0 9003 elxnn0 9066 elnn1uz2 9428 nn01to3 9436 elxr 9593 xaddcom 9674 xnegdi 9681 xpncan 9684 xleadd1a 9686 lcmdvds 11796 mulgcddvds 11811 cncongr2 11821 bj-peano4 13324 apdifflemr 13415 |
Copyright terms: Public domain | W3C validator |