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

Theorem orim2i 518
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 516 1  |-  ( ( ch  \/  ph )  ->  ( ch  \/  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    \/ wo 368
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 370
This theorem is referenced by:  orbi2i  519  pm1.5  522  pm2.3  572  r19.44av  2976  elpwunsn  4018  elsuci  4886  ordnbtwn  4910  infxpenlem  8284  fin1a2lem12  8684  fin1a2  8688  entri3  8827  zindd  10847  hashnn0pnf  12223  limccnp  21492  tgldimor  23083  ex-natded5.7-2  23764  gxsuc  23904  chirredi  25943  meran1  28394  dissym1  28404  ordtoplem  28418  ordcmp  28430  bj-dfif5ALT  32389
  Copyright terms: Public domain W3C validator