Theorem orbi2i 517

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 194	. . 3 |- ( ph -> ps )
3	2	orim2i 516	. 2 |- ( ( ch \/ ph ) -> ( ch \/ ps ) )
4	1	biimpri 206	. . 3 |- ( ps -> ph )
5	4	orim2i 516	. 2 |- ( ( ch \/ ps ) -> ( ch \/ ph ) )
6	3, 5	impbii 187	1 |- ( ( ch \/ ph ) <-> ( ch \/ ps ) )

Syntax hints:   <-> wb 184   \/ wo 366

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 185  df-or 368

This theorem is referenced by:  orbi1i  518  orbi12i  519  orass  522  or4  526  or42  527  orordir  529  dn1  967  3orcomb  984  excxor  1372  dfifp6  1392  cad1OLD  1484  19.44v  1794  nf4  1990  19.44  1997  exmidneOLD  2609  r19.30  2952  sspsstri  3545  unass  3600  undi  3697  undif3  3711  undif4  3826  ssunpr  4134  sspr  4135  sstp  4136  iinun2  4337  iinuni  4358  qfto  5209  somin1  5221  ordtri2  5445  on0eqel  5527  frxp  6894  wfrlem14  7034  wfrlem15  7035  supgtoreq  7962  wemapsolem  8009  fin1a2lem12  8823  psslinpr  9439  suplem2pr  9461  fimaxre  10530  elnn0  10838  elnn1uz2  11203  elxr  11378  xrinfmss  11554  elfzp1  11785  hashf1lem2  12554  dvdslelem  14239  pythagtrip  14567  tosso  15990  maducoeval2  19434  madugsum  19437  ist0-3  20139  limcdif  22572  ellimc2  22573  limcmpt  22579  limcres  22582  plydivex  22985  taylfval  23046  legtrid  24361  legso  24369  lmicom  24544  nb3graprlem2  24869  numclwwlk3lem  25525  atomli  27714  atoml2i  27715  or3di  27780  disjnf  27863  disjex  27884  disjexc  27885  orngsqr  28247  ind1a  28468  esumcvg  28533  voliune  28678  volfiniune  28679  bnj964  29328  dfso2  29967  socnv  29978  soseq  30065  lineunray  30485  bj-dfbi4  30720  bj-nf3  30761  itg2addnclem2  31440  tsxo1  31826  tsxo2  31827  tsxo3  31828  tsxo4  31829  tsna1  31833  tsna2  31834  tsna3  31835  ts3an1  31839  ts3an2  31840  ts3an3  31841  ts3or1  31842  ts3or2  31843  ts3or3  31844  prtlem90  31880  ifpim123g  35591  ifpor123g  35599  rp-fakeoranass  35605  frege133d  35744  undif3VD  36713  wallispilem3  37217  iccpartgt  37694  nnsum4primeseven  37848  nnsum4primesevenALTV  37849  pr1eqbg  37930  lindslinindsimp2  38575