Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > orim12i | GIF 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: → wi 4 ∨ wo 698 |
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 1375 19.43 1608 eueq3dc 2886 inssun 3348 abvor0dc 3418 ifmdc 3543 undifexmid 4156 pwssunim 4246 ordtriexmid 4482 ontriexmidim 4483 ordtri2orexmid 4484 ontr2exmid 4486 onsucsssucexmid 4488 onsucelsucexmid 4491 ordsoexmid 4523 0elsucexmid 4526 ordpwsucexmid 4531 ordtri2or2exmid 4532 ontri2orexmidim 4533 funcnvuni 5241 oprabidlem 5854 2oconcl 6388 inffiexmid 6853 unfiexmid 6864 ctssexmid 7095 exmidonfinlem 7130 sup3exmid 8833 zeo 9274 ef0lem 11568 |
Copyright terms: Public domain | W3C validator |