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 729 | . 2 ⊢ (𝜑 → (𝜓 ∨ 𝜃)) |
3 | orim12i.2 | . . 3 ⊢ (𝜒 → 𝜃) | |
4 | 3 | olcd 730 | . 2 ⊢ (𝜒 → (𝜓 ∨ 𝜃)) |
5 | 2, 4 | jaoi 712 | 1 ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∨ wo 704 |
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 705 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: orim1i 756 orim2i 757 dcim 837 pm5.12dc 906 pm5.14dc 907 pm5.55dc 909 pm5.54dc 914 prlem2 970 xordc1 1389 19.43 1622 eueq3dc 2905 inssun 3368 abvor0dc 3439 ifmdc 3566 undifexmid 4180 pwssunim 4270 ordtriexmid 4506 ontriexmidim 4507 ordtri2orexmid 4508 ontr2exmid 4510 onsucsssucexmid 4512 onsucelsucexmid 4515 ordsoexmid 4547 0elsucexmid 4550 ordpwsucexmid 4555 ordtri2or2exmid 4556 ontri2orexmidim 4557 funcnvuni 5269 oprabidlem 5888 2oconcl 6422 inffiexmid 6888 unfiexmid 6899 ctssexmid 7130 exmidonfinlem 7174 sup3exmid 8877 zeo 9321 ef0lem 11627 |
Copyright terms: Public domain | W3C validator |