Theorem orbi2i 519

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

Assertion

Ref	Expression
orbi2i

Proof of Theorem orbi2i

Step	Hyp	Ref	Expression
1		orbi2i.1	. . . 4
2	1	biimpi 194	. . 3
3	2	orim2i 518	. 2
4	1	biimpri 206	. . 3
5	4	orim2i 518	. 2
6	3, 5	impbii 188	1

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

This theorem is referenced by:  orbi1i  520  orbi12i  521  orass  524  or4  528  or42  529  orordir  531  dn1  966  3orcomb  983  excxor  1368  dfifp6  1386  cad1  1465  19.44v  1770  nf4  1962  19.44  1969  exmidneOLD  2663  r19.30  3002  sspsstri  3605  unass  3660  undi  3744  undif3  3758  undif4  3883  ssunpr  4192  sspr  4193  sstp  4194  iinun2  4396  iinuni  4414  ordtri2  4918  on0eqel  5000  qfto  5393  somin1  5408  frxp  6910  supgtoreq  7949  wemapsolem  7996  fin1a2lem12  8812  psslinpr  9430  suplem2pr  9452  fimaxre  10515  elnn0  10822  elnn1uz2  11187  elxr  11354  xrinfmss  11530  elfzp1  11759  hashf1lem2  12505  dvdslelem  14030  pythagtrip  14358  tosso  15666  maducoeval2  19142  madugsum  19145  ist0-3  19846  limcdif  22280  ellimc2  22281  limcmpt  22287  limcres  22290  plydivex  22693  taylfval  22754  legtrid  23978  legso  23985  lmicom  24154  nb3graprlem2  24452  numclwwlk3lem  25108  atomli  27301  atoml2i  27302  or3di  27367  disjnf  27433  disjex  27451  disjexc  27452  orngsqr  27794  ind1a  28034  esumcvg  28092  voliune  28201  volfiniune  28202  dfso2  29183  socnv  29194  soseq  29334  wfrlem14  29356  wfrlem15  29357  lineunray  29797  itg2addnclem2  30067  tsxo1  30544  tsxo2  30545  tsxo3  30546  tsxo4  30547  tsna1  30551  tsna2  30552  tsna3  30553  ts3an1  30557  ts3an2  30558  ts3an3  30559  ts3or1  30560  ts3or2  30561  ts3or3  30562  prtlem90  30598  wallispilem3  31849  pr1eqbg  32297  lindslinindsimp2  33064  undif3VD  33682  bnj964  34001  bj-dfbi4  34154  bj-nf3  34197  bj-ifim123g  37706  bj-ifor123g  37725  rp-fakeoranass  37738

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 370