![]() |
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 733 | . 2 ⊢ (𝜑 → (𝜓 ∨ 𝜃)) |
3 | orim12i.2 | . . 3 ⊢ (𝜒 → 𝜃) | |
4 | 3 | olcd 734 | . 2 ⊢ (𝜒 → (𝜓 ∨ 𝜃)) |
5 | 2, 4 | jaoi 716 | 1 ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∨ wo 708 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: orim1i 760 orim2i 761 dcim 841 pm5.12dc 910 pm5.14dc 911 pm5.55dc 913 pm5.54dc 918 prlem2 974 xordc1 1393 19.43 1628 eueq3dc 2912 inssun 3376 abvor0dc 3447 ifmdc 3575 undifexmid 4194 pwssunim 4285 ordtriexmid 4521 ontriexmidim 4522 ordtri2orexmid 4523 ontr2exmid 4525 onsucsssucexmid 4527 onsucelsucexmid 4530 ordsoexmid 4562 0elsucexmid 4565 ordpwsucexmid 4570 ordtri2or2exmid 4571 ontri2orexmidim 4572 funcnvuni 5286 oprabidlem 5906 2oconcl 6440 inffiexmid 6906 unfiexmid 6917 ctssexmid 7148 exmidonfinlem 7192 sup3exmid 8914 zeo 9358 ef0lem 11668 |
Copyright terms: Public domain | W3C validator |