Theorem orbi2i 526

Description: Inference adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-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

Step	Hyp	Ref	Expression
1		orbi2i.1	. . . 4 |- ( ph <-> ps )
2	1	biimpi 199	. . 3 |- ( ph -> ps )
3	2	orim2i 525	. 2 |- ( ( ch \/ ph ) -> ( ch \/ ps ) )
4	1	biimpri 211	. . 3 |- ( ps -> ph )
5	4	orim2i 525	. 2 |- ( ( ch \/ ps ) -> ( ch \/ ph ) )
6	3, 5	impbii 192	1 |- ( ( ch \/ ph ) <-> ( ch \/ ps ) )

Syntax hints:   <-> wb 189   \/ wo 374

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 190  df-or 376

This theorem is referenced by:  orbi1i  527  orbi12i  528  orass  531  or4  535  or42  536  orordir  538  dn1  983  3orcomb  1001  excxor  1421  dfifp6  1441  19.44v  1838  nf4  2053  19.44  2059  r19.30  2946  sspsstri  3546  unass  3602  undi  3701  undif3  3715  undif4  3832  ssunpr  4146  sspr  4147  sstp  4148  iinun2  4357  iinuni  4378  qfto  5239  somin1  5251  ordtri2  5476  on0eqel  5558  frxp  6932  wfrlem14  7074  wfrlem15  7075  supgtoreq  8011  wemapsolem  8090  fin1a2lem12  8866  psslinpr  9481  suplem2pr  9503  fimaxre  10578  elnn0  10899  elnn1uz2  11263  elxr  11444  xrinfmss  11623  elfzp1  11874  hashf1lem2  12651  dvdslelem  14397  pythagtrip  14832  tosso  16330  maducoeval2  19713  madugsum  19716  ist0-3  20409  limcdif  22879  ellimc2  22880  limcmpt  22886  limcres  22889  plydivex  23298  taylfval  23362  legtrid  24684  legso  24692  lmicom  24878  nb3graprlem2  25228  numclwwlk3lem  25884  atomli  28083  atoml2i  28084  or3di  28149  disjnf  28229  disjex  28250  disjexc  28251  orngsqr  28615  ind1a  28890  esumcvg  28955  voliune  29100  volfiniune  29101  bnj964  29802  dfso2  30442  socnv  30453  soseq  30540  lineunray  30962  bj-dfbi4  31193  bj-nf3  31237  poimirlem18  32002  poimirlem23  32007  poimirlem27  32011  poimirlem31  32015  itg2addnclem2  32038  tsxo1  32423  tsxo2  32424  tsxo3  32425  tsxo4  32426  tsna1  32430  tsna2  32431  tsna3  32432  ts3an1  32436  ts3an2  32437  ts3an3  32438  ts3or1  32439  ts3or2  32440  ts3or3  32441  prtlem90  32475  ifpim123g  36188  ifpor123g  36196  rp-fakeoranass  36202  frege133d  36401  undif3VD  37318  wallispilem3  37966  iccpartgt  38778  nnsum4primeseven  38932  nnsum4primesevenALTV  38933  pr1eqbg  39030  elxnn0  39117  nb3grprlem2  39504  lindslinindsimp2  40528