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  957  jaoi2OLD  960  3orcomb  975  excxor  1355  cad1  1440  nf4  1890  19.44  1897  exmidne  2612  r19.30  2863  sspsstri  3456  unass  3511  undi  3595  undif3  3609  undif4  3733  ssunpr  4033  sspr  4034  sstp  4035  iinun2  4234  iinuni  4252  ordtri2  4752  on0eqel  4834  qfto  5217  somin1  5232  frxp  6680  wemapsolem  7762  fin1a2lem12  8578  psslinpr  9198  suplem2pr  9220  fimaxre  10275  elnn0  10579  elnn1uz2  10929  elxr  11094  xrinfmss  11270  elfzp1  11503  hashf1lem2  12207  dvdslelem  13575  pythagtrip  13899  tosso  15204  maducoeval2  18444  madugsum  18447  ist0-3  18947  limcdif  21349  ellimc2  21350  limcmpt  21356  limcres  21359  plydivex  21761  taylfval  21822  legtrid  23020  nb3graprlem2  23358  atomli  25784  atoml2i  25785  or3di  25850  disjnf  25914  disjex  25932  disjexc  25933  orngsqr  26270  ind1a  26475  esumcvg  26533  voliune  26643  volfiniune  26644  dfso2  27562  socnv  27573  soseq  27713  wfrlem14  27735  wfrlem15  27736  lineunray  28176  itg2addnclem2  28441  tsbi4  28944  tsxo1  28945  tsxo2  28946  tsxo3  28947  tsxo4  28948  tsna1  28952  tsna2  28953  tsna3  28954  ts3an1  28958  ts3an2  28959  ts3an3  28960  ts3or1  28961  ts3or2  28962  ts3or3  28963  prtlem90  28999  wallispilem3  29859  pr1eqbg  30118  numclwwlk3lem  30698  supgtoreq  30740  lindslinindsimp2  30994  undif3VD  31615  bnj964  31933  bj-dfbi4  32074  bj-dfif6  32084  bj-nf3  32131