![]() |
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 120 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | orim2i 761 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1 | biimpri 133 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | orim2i 761 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | impbii 126 |
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 106 ax-ia2 107 ax-ia3 108 ax-io 709 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: orbi1i 763 orbi12i 764 orass 767 or4 771 or42 772 orordir 774 dcnnOLD 849 orbididc 953 3orcomb 987 excxor 1378 xordc 1392 nf4dc 1670 nf4r 1671 19.44 1682 dveeq2 1815 dvelimALT 2010 dvelimfv 2011 dvelimor 2018 dcne 2358 unass 3292 undi 3383 undif3ss 3396 symdifxor 3401 undif4 3485 iinuniss 3969 ordsucim 4499 suc11g 4556 qfto 5018 nntri3or 6493 reapcotr 8554 elnn0 9177 elxnn0 9240 elnn1uz2 9606 nn01to3 9616 elxr 9775 xaddcom 9860 xnegdi 9867 xpncan 9870 xleadd1a 9872 lcmdvds 12078 mulgcddvds 12093 cncongr2 12103 pythagtrip 12282 bj-peano4 14677 apdifflemr 14765 |
Copyright terms: Public domain | W3C validator |