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

Theorem orim2i 516
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 22 . 2  |-  ( ch 
->  ch )
2 orim1i.1 . 2  |-  ( ph  ->  ps )
31, 2orim12i 514 1  |-  ( ( ch  \/  ph )  ->  ( ch  \/  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 366
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 185  df-or 368
This theorem is referenced by:  orbi2i  517  pm1.5  520  pm2.3  570  r19.44v  3011  elpwunsn  4057  elsuci  4933  ordnbtwn  4957  infxpenlem  8382  fin1a2lem12  8782  fin1a2  8786  entri3  8925  zindd  10961  hashnn0pnf  12397  limccnp  22461  tgldimor  24094  ex-natded5.7-2  25335  gxsuc  25472  chirredi  27511  meran1  30104  dissym1  30114  ordtoplem  30128  ordcmp  30140
  Copyright terms: Public domain W3C validator