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  1800  19.44  1813  exmidne  2452  r19.30  2685  sspsstri  3278  unass  3332  undi  3416  undif3  3429  undif4  3511  ssunpr  3776  sspr  3777  sstp  3778  iinun2  3968  iinuni  3985  ordtri2  4427  trsuc2OLD  4477  on0eqel  4510  qfto  5064  somin1  5079  frxp  6225  wemapso2lem  7265  fin1a2lem12  8037  psslinpr  8655  suplem2pr  8677  fimaxre  9701  elnn0  9967  elnn1uz2  10294  elxr  10458  xrinfmss  10628  elfzp1  10836  hashf1lem2  11394  dvdslelem  12573  pythagtrip  12887  tosso  14142  ist0-3  17073  limcdif  19226  ellimc2  19227  limcmpt  19233  limcres  19236  plydivex  19677  taylfval  19738  atomli  22962  atoml2i  22963  or3di  23123  disjex  23176  disjexc  23177  esumcvg  23454  ind1a  23604  dfso2  24111  soseq  24254  wfrlem14  24269  wfrlem15  24270  lineunray  24770  prtlem90  26723  wallispilem3  27816  undif3VD  28658  bnj964  28975
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