![]() |
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 690 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | orim12i.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | olcd 691 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | jaoi 674 |
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 105 ax-ia2 106 ax-ia3 107 ax-io 668 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: orim1i 715 orim2i 716 dcim 825 pm5.12dc 857 pm5.14dc 858 pm5.55dc 860 pm5.54dc 868 prlem2 923 xordc1 1336 19.43 1571 eueq3dc 2803 inssun 3255 abvor0dc 3325 ifmdc 3448 undifexmid 4049 pwssunim 4135 ordtriexmid 4366 ordtri2orexmid 4367 ontr2exmid 4369 onsucsssucexmid 4371 onsucelsucexmid 4374 ordsoexmid 4406 0elsucexmid 4409 ordpwsucexmid 4414 ordtri2or2exmid 4415 funcnvuni 5117 oprabidlem 5718 2oconcl 6241 inffiexmid 6702 unfiexmid 6708 djur 6837 djuun 6840 sup3exmid 8515 zeo 8950 ef0lem 11099 |
Copyright terms: Public domain | W3C validator |