MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orbi2i Structured version   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  1318  cad1  1407  nf4  1891  19.44  1898  exmidne  2604  r19.30  2845  sspsstri  3441  unass  3496  undi  3580  undif3  3594  undif4  3676  ssunpr  3953  sspr  3954  sstp  3955  iinun2  4149  iinuni  4166  ordtri2  4608  on0eqel  4691  qfto  5247  somin1  5262  frxp  6448  wemapso2lem  7511  fin1a2lem12  8283  psslinpr  8900  suplem2pr  8922  fimaxre  9947  elnn0  10215  elnn1uz2  10544  elxr  10708  xrinfmss  10880  elfzp1  11089  hashf1lem2  11697  dvdslelem  12886  pythagtrip  13200  tosso  14457  ist0-3  17401  limcdif  19755  ellimc2  19756  limcmpt  19762  limcres  19765  plydivex  20206  taylfval  20267  nb3graprlem2  21453  atomli  23877  atoml2i  23878  or3di  23943  disjex  24024  disjexc  24025  ofldsqr  24232  ind1a  24410  esumcvg  24468  voliune  24577  volfiniune  24578  dfso2  25369  socnv  25380  soseq  25521  wfrlem14  25543  wfrlem15  25544  lineunray  26073  itg2addnclem2  26247  prtlem90  26687  wallispilem3  27773  pr1eqbg  28036  undif3VD  28921  bnj964  29241
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