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 406 | . 2 ⊢ (𝜑 → (𝜓 ∨ 𝜃)) |
3 | orim12i.2 | . . 3 ⊢ (𝜒 → 𝜃) | |
4 | 3 | olcd 407 | . 2 ⊢ (𝜒 → (𝜓 ∨ 𝜃)) |
5 | 2, 4 | jaoi 393 | 1 ⊢ ((𝜑 ∨ 𝜒) → (𝜓 ∨ 𝜃)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 382 |
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 196 df-or 384 |
This theorem is referenced by: orim1i 538 orim2i 539 prlem2 998 ifpor 1015 eueq3 3348 pwssun 4944 xpima 5495 funcnvuni 7012 2oconcl 7470 fin23lem23 9031 fin23lem19 9041 fin1a2lem13 9117 fin1a2s 9119 nn0ge0 11195 hash2pwpr 13115 trclfvg 13604 mreexexdOLD 16132 xpcbas 16641 odcl 17778 gexcl 17818 ang180lem4 24342 cusgrares 26001 2pthlem2 26126 elim2ifim 28748 locfinref 29236 volmeas 29621 nepss 30854 funpsstri 30909 fvresval 30911 dvasin 32666 dvacos 32667 relexpxpmin 37028 clsk1indlem3 37361 elfzlmr 40366 resolution 42354 |
Copyright terms: Public domain | W3C validator |