MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orim2i 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  2808  elsuci  4589  ordnbtwn  4613  elpwunsn  4698  infxpenlem  7829  fin1a2lem12  8225  fin1a2  8229  entri3  8368  zindd  10304  hashnn0pnf  11554  limccnp  19646  gxsuc  21709  chirredi  23746  meran1  25876  dissym1  25886  ordtoplem  25900  ordcmp  25912
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