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 869 | . 2 ⊢ (𝜑 → (𝜓 ∨ 𝜃)) |
3 | orim12i.2 | . . 3 ⊢ (𝜒 → 𝜃) | |
4 | 3 | olcd 870 | . 2 ⊢ (𝜒 → (𝜓 ∨ 𝜃)) |
5 | 2, 4 | jaoi 851 | 1 ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 841 |
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 208 df-or 842 |
This theorem is referenced by: orim1i 903 orim2i 904 prlem2 1047 ifpor 1063 eueq3 3699 pwssun 5448 xpima 6032 0mpo0 7226 funcnvuni 7625 2oconcl 8117 djur 9336 djuun 9343 fin23lem23 9736 fin23lem19 9746 fin1a2lem13 9822 fin1a2s 9824 nn0ge0 11910 elfzlmr 13139 hash2pwpr 13822 trclfvg 14363 xpcbas 17416 odcl 18593 gexcl 18634 ang180lem4 25317 elim2ifim 30227 locfinref 31004 volmeas 31389 nepss 32845 funpsstri 32905 fvresval 32907 dvasin 34859 dvacos 34860 disjorimxrn 35858 relexpxpmin 39940 clsk1indlem3 40271 elsprel 43514 resolution 44828 |
Copyright terms: Public domain | W3C validator |