![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > orim2i | Structured version Visualization version GIF version |
Description: Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.) |
Ref | Expression |
---|---|
orim1i.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
orim2i | ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 ⊢ (𝜒 → 𝜒) | |
2 | orim1i.1 | . 2 ⊢ (𝜑 → 𝜓) | |
3 | 1, 2 | orim12i 906 | 1 ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 845 |
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 846 |
This theorem is referenced by: orbi2i 910 pm1.5 917 pm2.3 922 r19.44v 3183 elpwunsn 4689 elsuci 6438 infxpenlem 10038 fin1a2lem12 10436 fin1a2 10440 entri3 10584 zindd 12696 elfzr 13781 hashnn0pnf 14337 limccnp 25864 tgldimor 28378 ex-natded5.7-2 30294 chirredi 32276 meran1 36026 dissym1 36036 ordtoplem 36050 ordcmp 36062 poimirlem31 37255 simpcntrab 46396 setc2othin 48248 |
Copyright terms: Public domain | W3C validator |