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

Theorem orim2i 908
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 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