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

Theorem orim2i 888
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 886 1 ((𝜒𝜑) → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 828
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 829
This theorem is referenced by:  orbi2i  890  pm1.5  897  pm2.3  902  r19.44v  3242  elpwunsn  4363  elsuci  5935  ordnbtwnOLD  5961  infxpenlem  9037  fin1a2lem12  9436  fin1a2  9440  entri3  9584  zindd  11681  elfzr  12790  hashnn0pnf  13335  limccnp  23876  tgldimor  25619  ex-natded5.7-2  27612  chirredi  29594  meran1  32748  dissym1  32758  ordtoplem  32772  ordcmp  32784  poimirlem31  33774
  Copyright terms: Public domain W3C validator