|   | 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 908 | 1 ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ∨ wo 847 | 
| 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 848 | 
| This theorem is referenced by: orbi2i 912 pm1.5 919 pm2.3 924 r19.44v 3193 elpwunsn 4683 elsuci 6450 infxpenlem 10054 fin1a2lem12 10452 fin1a2 10456 entri3 10600 zindd 12721 elfzr 13820 hashnn0pnf 14382 limccnp 25927 tgldimor 28511 ex-natded5.7-2 30432 chirredi 32414 meran1 36413 dissym1 36423 ordtoplem 36437 ordcmp 36449 poimirlem31 37659 simpcntrab 46890 setc2othin 49138 | 
| Copyright terms: Public domain | W3C validator |