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

Theorem orim2i 539
 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 537 1 ((𝜒𝜑) → (𝜒𝜓))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 382 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 196  df-or 384 This theorem is referenced by:  orbi2i  540  pm1.5  543  pm2.3  594  r19.44v  3075  elpwunsn  4171  elsuci  5708  ordnbtwnOLD  5734  infxpenlem  8719  fin1a2lem12  9116  fin1a2  9120  entri3  9260  zindd  11354  hashnn0pnf  12992  limccnp  23461  tgldimor  25197  ex-natded5.7-2  26661  chirredi  28637  meran1  31580  dissym1  31590  ordtoplem  31604  ordcmp  31616  poimirlem31  32610  elfzr  40364
 Copyright terms: Public domain W3C validator