![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > orim12i | Structured version Visualization version 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 872 | . 2 ⊢ (𝜑 → (𝜓 ∨ 𝜃)) |
3 | orim12i.2 | . . 3 ⊢ (𝜒 → 𝜃) | |
4 | 3 | olcd 873 | . 2 ⊢ (𝜒 → (𝜓 ∨ 𝜃)) |
5 | 2, 4 | jaoi 856 | 1 ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 846 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 206 df-or 847 |
This theorem is referenced by: orim1i 909 orim2i 910 prlem2 1055 ifpor 1072 eueq3 3674 pwssun 5533 xpima 6139 fvresval 7308 0mpo0 7445 funcnvuni 7873 2oconcl 8454 djur 9862 djuun 9869 fin23lem23 10269 fin23lem19 10279 fin1a2lem13 10355 fin1a2s 10357 nn0ge0 12445 elfzlmr 13693 hash2pwpr 14382 trclfvg 14907 xpcbas 18073 odcl 19325 gexcl 19369 ang180lem4 26178 sltn0 27256 elim2ifim 31509 locfinref 32462 volmeas 32870 nepss 34329 funpsstri 34379 bj-prmoore 35615 bj-imdirco 35690 dvasin 36191 dvacos 36192 disjorimxrn 37239 relexpxpmin 42063 clsk1indlem3 42389 elsprel 45741 resolution 47320 |
Copyright terms: Public domain | W3C validator |