![]() |
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 723 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | orim12i.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | olcd 724 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | jaoi 706 |
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: orim1i 750 orim2i 751 dcim 827 pm5.12dc 896 pm5.14dc 897 pm5.55dc 899 pm5.54dc 904 prlem2 959 xordc1 1372 19.43 1608 eueq3dc 2862 inssun 3321 abvor0dc 3391 ifmdc 3514 undifexmid 4125 pwssunim 4214 ordtriexmid 4445 ordtri2orexmid 4446 ontr2exmid 4448 onsucsssucexmid 4450 onsucelsucexmid 4453 ordsoexmid 4485 0elsucexmid 4488 ordpwsucexmid 4493 ordtri2or2exmid 4494 funcnvuni 5200 oprabidlem 5810 2oconcl 6344 inffiexmid 6808 unfiexmid 6814 ctssexmid 7032 exmidonfinlem 7066 sup3exmid 8739 zeo 9180 ef0lem 11403 |
Copyright terms: Public domain | W3C validator |