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

Theorem orim2i 909
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 907 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  911  pm1.5  918  pm2.3  923  r19.44v  3193  elpwunsn  4687  elsuci  6431  infxpenlem  10007  fin1a2lem12  10405  fin1a2  10409  entri3  10553  zindd  12662  elfzr  13744  hashnn0pnf  14301  limccnp  25407  tgldimor  27750  ex-natded5.7-2  29662  chirredi  31642  meran1  35291  dissym1  35301  ordtoplem  35315  ordcmp  35327  poimirlem31  36514  simpcntrab  45576  setc2othin  47666
  Copyright terms: Public domain W3C validator