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

Theorem orbi2i 506
Description: Inference adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Dec-2012.)
Hypothesis
Ref Expression
orbi2i.1  |-  ( ph  <->  ps )
Assertion
Ref Expression
orbi2i  |-  ( ( ch  \/  ph )  <->  ( ch  \/  ps )
)

Proof of Theorem orbi2i
StepHypRef Expression
1 orbi2i.1 . . . 4  |-  ( ph  <->  ps )
21biimpi 187 . . 3  |-  ( ph  ->  ps )
32orim2i 505 . 2  |-  ( ( ch  \/  ph )  ->  ( ch  \/  ps ) )
41biimpri 198 . . 3  |-  ( ps 
->  ph )
54orim2i 505 . 2  |-  ( ( ch  \/  ps )  ->  ( ch  \/  ph ) )
63, 5impbii 181 1  |-  ( ( ch  \/  ph )  <->  ( ch  \/  ps )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 177    \/ wo 358
This theorem is referenced by:  orbi1i  507  orbi12i  508  orass  511  or4  515  or42  516  orordir  518  dn1  933  jaoi2  934  3orcomb  946  excxor  1315  cad1  1404  nf4  1887  19.44  1894  exmidne  2573  r19.30  2813  sspsstri  3409  unass  3464  undi  3548  undif3  3562  undif4  3644  ssunpr  3921  sspr  3922  sstp  3923  iinun2  4117  iinuni  4134  ordtri2  4576  on0eqel  4658  qfto  5214  somin1  5229  frxp  6415  wemapso2lem  7475  fin1a2lem12  8247  psslinpr  8864  suplem2pr  8886  fimaxre  9911  elnn0  10179  elnn1uz2  10508  elxr  10672  xrinfmss  10844  elfzp1  11053  hashf1lem2  11660  dvdslelem  12849  pythagtrip  13163  tosso  14420  ist0-3  17363  limcdif  19716  ellimc2  19717  limcmpt  19723  limcres  19726  plydivex  20167  taylfval  20228  nb3graprlem2  21414  atomli  23838  atoml2i  23839  or3di  23904  disjex  23985  disjexc  23986  ofldsqr  24193  ind1a  24371  esumcvg  24429  voliune  24538  volfiniune  24539  dfso2  25325  soseq  25468  wfrlem14  25483  wfrlem15  25484  lineunray  25985  itg2addnclem2  26156  prtlem90  26596  wallispilem3  27683  pr1eqbg  27944  undif3VD  28703  bnj964  29020
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