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 844
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 210  df-or 845
This theorem is referenced by:  orbi2i  910  pm1.5  917  pm2.3  922  r19.44v  3337  elpwunsn  4594  elsuci  6230  infxpenlem  9416  fin1a2lem12  9810  fin1a2  9814  entri3  9958  zindd  12061  elfzr  13133  hashnn0pnf  13686  limccnp  24473  tgldimor  26275  ex-natded5.7-2  28176  chirredi  30156  meran1  33767  dissym1  33777  ordtoplem  33791  ordcmp  33803  poimirlem31  34970  simpcntrab  43303
  Copyright terms: Public domain W3C validator