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  3orcomb  982  excxor  1367  cad1  1451  nf4  1946  19.44  1953  exmidneOLD  2647  r19.30  2986  sspsstri  3589  unass  3644  undi  3728  undif3  3742  undif4  3866  ssunpr  4174  sspr  4175  sstp  4176  iinun2  4378  iinuni  4396  ordtri2  4900  on0eqel  4982  qfto  5375  somin1  5390  frxp  6892  supgtoreq  7928  wemapsolem  7975  fin1a2lem12  8791  psslinpr  9409  suplem2pr  9431  fimaxre  10493  elnn0  10800  elnn1uz2  11164  elxr  11331  xrinfmss  11507  elfzp1  11736  hashf1lem2  12481  dvdslelem  13904  pythagtrip  14232  tosso  15537  maducoeval2  19012  madugsum  19015  ist0-3  19716  limcdif  22150  ellimc2  22151  limcmpt  22157  limcres  22160  plydivex  22562  taylfval  22623  legtrid  23847  legso  23854  lmicom  24023  nb3graprlem2  24321  numclwwlk3lem  24977  atomli  27170  atoml2i  27171  or3di  27236  disjnf  27302  disjex  27320  disjexc  27321  orngsqr  27664  ind1a  27904  esumcvg  27962  voliune  28071  volfiniune  28072  dfso2  29155  socnv  29166  soseq  29306  wfrlem14  29328  wfrlem15  29329  lineunray  29769  itg2addnclem2  30039  tsxo1  30516  tsxo2  30517  tsxo3  30518  tsxo4  30519  tsna1  30523  tsna2  30524  tsna3  30525  ts3an1  30529  ts3an2  30530  ts3an3  30531  ts3or1  30532  ts3or2  30533  ts3or3  30534  prtlem90  30570  wallispilem3  31738  pr1eqbg  32135  lindslinindsimp2  32794  undif3VD  33410  bnj964  33729  bj-dfbi4  33870  bj-dfif6  33885  bj-nf3  33932  rp-fakeoranass  37424