![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > orim12i | Unicode version |
Description: Disjoin antecedents and consequents of two premises. (Contributed by NM, 6-Jun-1994.) (Proof shortened by Wolf Lammen, 25-Jul-2012.) |
Ref | Expression |
---|---|
orim12i.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
orim12i.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
orim12i |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orim12i.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | orcd 685 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | orim12i.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | olcd 686 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | jaoi 669 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-io 663 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: orim1i 710 orim2i 711 dcim 818 pm5.12dc 850 pm5.14dc 851 pm5.55dc 853 pm5.54dc 861 prlem2 916 xordc1 1325 19.43 1560 eueq3dc 2767 inssun 3211 abvor0dc 3276 pwssunim 4047 ordtriexmid 4273 ordtri2orexmid 4274 ontr2exmid 4276 onsucsssucexmid 4278 onsucelsucexmid 4281 ordsoexmid 4313 0elsucexmid 4316 ordpwsucexmid 4321 ordtri2or2exmid 4322 funcnvuni 4999 oprabidlem 5567 2oconcl 6086 unfiexmid 6438 zeo 8533 |
Copyright terms: Public domain | W3C validator |