![]() |
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 734 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | orim12i.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | olcd 735 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | jaoi 717 |
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 710 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: orim1i 761 orim2i 762 dcim 842 pm5.12dc 911 pm5.14dc 912 pm5.55dc 914 pm5.54dc 919 prlem2 976 xordc1 1404 19.43 1639 eueq3dc 2926 inssun 3390 abvor0dc 3461 ifmdc 3589 undifexmid 4211 pwssunim 4302 ordtriexmid 4538 ontriexmidim 4539 ordtri2orexmid 4540 ontr2exmid 4542 onsucsssucexmid 4544 onsucelsucexmid 4547 ordsoexmid 4579 0elsucexmid 4582 ordpwsucexmid 4587 ordtri2or2exmid 4588 ontri2orexmidim 4589 funcnvuni 5304 oprabidlem 5926 2oconcl 6463 inffiexmid 6933 unfiexmid 6945 ctssexmid 7177 exmidonfinlem 7221 sup3exmid 8943 zeo 9387 ef0lem 11699 |
Copyright terms: Public domain | W3C validator |