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 722 | . 2 |
3 | orim12i.2 | . . 3 | |
4 | 3 | olcd 723 | . 2 |
5 | 2, 4 | jaoi 705 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wo 697 |
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 698 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: orim1i 749 orim2i 750 dcim 826 pm5.12dc 895 pm5.14dc 896 pm5.55dc 898 pm5.54dc 903 prlem2 958 xordc1 1371 19.43 1607 eueq3dc 2853 inssun 3311 abvor0dc 3381 ifmdc 3504 undifexmid 4112 pwssunim 4201 ordtriexmid 4432 ordtri2orexmid 4433 ontr2exmid 4435 onsucsssucexmid 4437 onsucelsucexmid 4440 ordsoexmid 4472 0elsucexmid 4475 ordpwsucexmid 4480 ordtri2or2exmid 4481 funcnvuni 5187 oprabidlem 5795 2oconcl 6329 inffiexmid 6793 unfiexmid 6799 ctssexmid 7017 exmidonfinlem 7042 sup3exmid 8708 zeo 9149 ef0lem 11355 |
Copyright terms: Public domain | W3C validator |