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

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

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

This theorem is referenced by:  orbi1i  520  orbi12i  521  orass  524  or4  528  or42  529  orordir  531  dn1  964  jaoi2OLD  967  3orcomb  983  excxor  1365  cad1  1450  nf4  1911  19.44  1918  exmidneOLD  2673  r19.30  3006  sspsstri  3606  unass  3661  undi  3745  undif3  3759  undif4  3883  ssunpr  4189  sspr  4190  sstp  4191  iinun2  4391  iinuni  4409  ordtri2  4913  on0eqel  4995  qfto  5388  somin1  5403  frxp  6893  supgtoreq  7928  wemapsolem  7975  fin1a2lem12  8791  psslinpr  9409  suplem2pr  9431  fimaxre  10490  elnn0  10797  elnn1uz2  11158  elxr  11325  xrinfmss  11501  elfzp1  11730  hashf1lem2  12471  dvdslelem  13889  pythagtrip  14217  tosso  15523  maducoeval2  18937  madugsum  18940  ist0-3  19640  limcdif  22043  ellimc2  22044  limcmpt  22050  limcres  22053  plydivex  22455  taylfval  22516  legtrid  23733  legso  23740  lmicom  23859  nb3graprlem2  24156  numclwwlk3lem  24813  atomli  27005  atoml2i  27006  or3di  27071  disjnf  27134  disjex  27152  disjexc  27153  orngsqr  27485  ind1a  27702  esumcvg  27760  voliune  27869  volfiniune  27870  dfso2  28788  socnv  28799  soseq  28939  wfrlem14  28961  wfrlem15  28962  lineunray  29402  itg2addnclem2  29672  tsbi4  30175  tsxo1  30176  tsxo2  30177  tsxo3  30178  tsxo4  30179  tsna1  30183  tsna2  30184  tsna3  30185  ts3an1  30189  ts3an2  30190  ts3an3  30191  ts3or1  30192  ts3or2  30193  ts3or3  30194  prtlem90  30230  wallispilem3  31395  pr1eqbg  31792  lindslinindsimp2  32163  undif3VD  32780  bnj964  33098  bj-dfbi4  33239  bj-dfif6  33249  bj-nf3  33298