MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orim2i 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
Assertion
Ref Expression
orim2i

Proof of Theorem orim2i
StepHypRef Expression
1 id 22 . 2
2 orim1i.1 . 2
31, 2orim12i 516 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  \/wo 368
This theorem is referenced by:  orbi2i  519  pm1.5  522  pm2.3  572  r19.44v  3014  elpwunsn  4070  elsuci  4949  ordnbtwn  4973  infxpenlem  8412  fin1a2lem12  8812  fin1a2  8816  entri3  8955  zindd  10990  hashnn0pnf  12415  limccnp  22295  tgldimor  23893  ex-natded5.7-2  25133  gxsuc  25274  chirredi  27313  meran1  29876  dissym1  29886  ordtoplem  29900  ordcmp  29912
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
  Copyright terms: Public domain W3C validator