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

Step	Hyp	Ref	Expression
1		orbi2i.1	. . . 4 |- ( ph <-> ps )
2	1	biimpi 187	. . 3 |- ( ph -> ps )
3	2	orim2i 505	. 2 |- ( ( ch \/ ph ) -> ( ch \/ ps ) )
4	1	biimpri 198	. . 3 |- ( ps -> ph )
5	4	orim2i 505	. 2 |- ( ( ch \/ ps ) -> ( ch \/ ph ) )
6	3, 5	impbii 181	1 |- ( ( ch \/ ph ) <-> ( ch \/ ps ) )

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