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

Theorem orim2i 896
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 894 1 ((𝜒𝜑) → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 836
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 837
This theorem is referenced by:  orbi2i  898  pm1.5  905  pm2.3  910  r19.44v  3242  elpwunsn  4363  elsuci  5933  ordnbtwnOLD  5959  infxpenlem  9040  fin1a2lem12  9439  fin1a2  9443  entri3  9587  zindd  11685  elfzr  12789  hashnn0pnf  13334  limccnp  23875  tgldimor  25618  ex-natded5.7-2  27611  chirredi  29593  meran1  32747  dissym1  32757  ordtoplem  32771  ordcmp  32783  poimirlem31  33773
  Copyright terms: Public domain W3C validator