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

Theorem orbi2i 505
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 186 . . 3  |-  ( ph  ->  ps )
32orim2i 504 . 2  |-  ( ( ch  \/  ph )  ->  ( ch  \/  ps ) )
41biimpri 197 . . 3  |-  ( ps 
->  ph )
54orim2i 504 . 2  |-  ( ( ch  \/  ps )  ->  ( ch  \/  ph ) )
63, 5impbii 180 1  |-  ( ( ch  \/  ph )  <->  ( ch  \/  ps )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 176    \/ wo 357
This theorem is referenced by:  orbi1i  506  orbi12i  507  orass  510  or4  514  or42  515  orordir  517  dn1  932  3orcomb  944  excxor  1300  cad1  1388  nf4  1812  19.44  1825  exmidne  2465  r19.30  2698  sspsstri  3291  unass  3345  undi  3429  undif3  3442  undif4  3524  ssunpr  3792  sspr  3793  sstp  3794  iinun2  3984  iinuni  4001  ordtri2  4443  trsuc2OLD  4493  on0eqel  4526  qfto  5080  somin1  5095  frxp  6241  wemapso2lem  7281  fin1a2lem12  8053  psslinpr  8671  suplem2pr  8693  fimaxre  9717  elnn0  9983  elnn1uz2  10310  elxr  10474  xrinfmss  10644  elfzp1  10852  hashf1lem2  11410  dvdslelem  12589  pythagtrip  12903  tosso  14158  ist0-3  17089  limcdif  19242  ellimc2  19243  limcmpt  19249  limcres  19252  plydivex  19693  taylfval  19754  atomli  22978  atoml2i  22979  or3di  23139  disjex  23192  disjexc  23193  esumcvg  23469  ind1a  23619  dfso2  24182  soseq  24325  wfrlem14  24340  wfrlem15  24341  lineunray  24842  itg2addnclem2  25004  prtlem90  26826  wallispilem3  27919  jaoi2  28176  nb3graprlem2  28288  undif3VD  28974  bnj964  29291
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 177  df-or 359
  Copyright terms: Public domain W3C validator