| 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 874 | . 2 ⊢ (𝜑 → (𝜓 ∨ 𝜃)) |
| 3 | orim12i.2 | . . 3 ⊢ (𝜒 → 𝜃) | |
| 4 | 3 | olcd 875 | . 2 ⊢ (𝜒 → (𝜓 ∨ 𝜃)) |
| 5 | 2, 4 | jaoi 858 | 1 ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∨ wo 848 |
| 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 207 df-or 849 |
| This theorem is referenced by: orim1i 910 orim2i 911 prlem2 1056 ifpor 1073 eueq3 3717 pwssun 5575 xpima 6202 fvresval 7378 0mpo0 7516 funcnvuni 7954 2oconcl 8541 djur 9959 djuun 9966 fin23lem23 10366 fin23lem19 10376 fin1a2lem13 10452 fin1a2s 10454 nn0ge0 12551 elfzlmr 13820 hash2pwpr 14515 trclfvg 15054 xpcbas 18223 odcl 19554 gexcl 19598 ang180lem4 26855 sltn0 27943 n0seo 28405 elim2ifim 32558 locfinref 33840 volmeas 34232 nepss 35718 funpsstri 35766 bj-prmoore 37116 bj-imdirco 37191 dvasin 37711 dvacos 37712 disjorimxrn 38749 relexpxpmin 43730 clsk1indlem3 44056 elsprel 47462 resolution 49318 |
| Copyright terms: Public domain | W3C validator |