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 684 | . 2 |
3 | orim12i.2 | . . 3 | |
4 | 3 | olcd 685 | . 2 |
5 | 2, 4 | jaoi 668 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wo 661 |
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 662 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: orim1i 709 orim2i 710 dcim 817 pm5.12dc 849 pm5.14dc 850 pm5.55dc 852 pm5.54dc 860 prlem2 915 xordc1 1324 19.43 1559 eueq3dc 2766 inssun 3204 abvor0dc 3269 pwssunim 4039 ordtriexmid 4265 ordtri2orexmid 4266 ontr2exmid 4268 onsucsssucexmid 4270 onsucelsucexmid 4273 ordsoexmid 4305 0elsucexmid 4308 ordpwsucexmid 4313 ordtri2or2exmid 4314 funcnvuni 4988 oprabidlem 5556 2oconcl 6045 zeo 8452 |
Copyright terms: Public domain | W3C validator |