![]() |
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 895 | 1 ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∨ wo 836 |
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 199 df-or 837 |
This theorem is referenced by: orbi2i 899 pm1.5 906 pm2.3 911 r19.44v 3280 elpwunsn 4452 elsuci 6042 infxpenlem 9169 fin1a2lem12 9568 fin1a2 9572 entri3 9716 zindd 11830 elfzr 12900 hashnn0pnf 13447 limccnp 24092 tgldimor 25853 ex-natded5.7-2 27844 chirredi 29825 meran1 32993 dissym1 33003 ordtoplem 33017 ordcmp 33029 poimirlem31 34066 |
Copyright terms: Public domain | W3C validator |