Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  orim2i Structured version   Visualization version   GIF version

Theorem orim2i 540
 Description: Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
Hypothesis
Ref Expression
orim1i.1 (𝜑𝜓)
Assertion
Ref Expression
orim2i ((𝜒𝜑) → (𝜒𝜓))

Proof of Theorem orim2i
StepHypRef Expression
1 id 22 . 2 (𝜒𝜒)
2 orim1i.1 . 2 (𝜑𝜓)
31, 2orim12i 538 1 ((𝜒𝜑) → (𝜒𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 383 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 197  df-or 385 This theorem is referenced by:  orbi2i  541  pm1.5  544  pm2.3  595  r19.44v  3087  elpwunsn  4200  elsuci  5755  ordnbtwnOLD  5781  infxpenlem  8788  fin1a2lem12  9185  fin1a2  9189  entri3  9333  zindd  11430  elfzr  12529  hashnn0pnf  13078  limccnp  23578  tgldimor  25314  ex-natded5.7-2  27140  chirredi  29123  meran1  32087  dissym1  32097  ordtoplem  32111  ordcmp  32123  poimirlem31  33107
 Copyright terms: Public domain W3C validator