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

Theorem orim2i 910
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 908 1 ((𝜒𝜑) → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 846
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 847
This theorem is referenced by:  orbi2i  912  pm1.5  919  pm2.3  924  r19.44v  3191  elpwunsn  4649  elsuci  6389  infxpenlem  9956  fin1a2lem12  10354  fin1a2  10358  entri3  10502  zindd  12611  elfzr  13692  hashnn0pnf  14249  limccnp  25271  tgldimor  27486  ex-natded5.7-2  29398  chirredi  31378  meran1  34912  dissym1  34922  ordtoplem  34936  ordcmp  34948  poimirlem31  36138  simpcntrab  45185  setc2othin  47150
  Copyright terms: Public domain W3C validator