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

Theorem orim2i 505
Description: Introduce disjunct to both sides of an implication. (Contributed by NM, 6-Jun-1994.)
Hypothesis
Ref Expression
orim1i.1  |-  ( ph  ->  ps )
Assertion
Ref Expression
orim2i  |-  ( ( ch  \/  ph )  ->  ( ch  \/  ps ) )

Proof of Theorem orim2i
StepHypRef Expression
1 id 20 . 2  |-  ( ch 
->  ch )
2 orim1i.1 . 2  |-  ( ph  ->  ps )
31, 2orim12i 503 1  |-  ( ( ch  \/  ph )  ->  ( ch  \/  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 358
This theorem is referenced by:  orbi2i  506  pm1.5  509  pm2.3  556  r19.44av  2856  elsuci  4639  ordnbtwn  4664  elpwunsn  4749  infxpenlem  7887  fin1a2lem12  8283  fin1a2  8287  entri3  8426  zindd  10363  hashnn0pnf  11618  limccnp  19770  gxsuc  21852  chirredi  23889  meran1  26153  dissym1  26163  ordtoplem  26177  ordcmp  26189
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-or 360
  Copyright terms: Public domain W3C validator