Theorem orbi2i 522

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 198	. . 3 |- ( ph -> ps )
3	2	orim2i 521	. 2 |- ( ( ch \/ ph ) -> ( ch \/ ps ) )
4	1	biimpri 210	. . 3 |- ( ps -> ph )
5	4	orim2i 521	. 2 |- ( ( ch \/ ps ) -> ( ch \/ ph ) )
6	3, 5	impbii 191	1 |- ( ( ch \/ ph ) <-> ( ch \/ ps ) )

Syntax hints:   <-> wb 188   \/ wo 370

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 189  df-or 372

This theorem is referenced by:  orbi1i  523  orbi12i  524  orass  527  or4  531  or42  532  orordir  534  dn1  975  3orcomb  993  excxor  1407  dfifp6  1427  19.44v  1818  nf4  2019  19.44  2025  exmidneOLD  2631  r19.30  2974  sspsstri  3568  unass  3624  undi  3721  undif3  3735  undif4  3850  ssunpr  4160  sspr  4161  sstp  4162  iinun2  4363  iinuni  4384  qfto  5238  somin1  5250  ordtri2  5475  on0eqel  5557  frxp  6915  wfrlem14  7055  wfrlem15  7056  supgtoreq  7990  wemapsolem  8069  fin1a2lem12  8843  psslinpr  9458  suplem2pr  9480  fimaxre  10553  elnn0  10873  elnn1uz2  11237  elxr  11418  xrinfmss  11597  elfzp1  11848  hashf1lem2  12618  dvdslelem  14342  pythagtrip  14777  tosso  16275  maducoeval2  19657  madugsum  19660  ist0-3  20353  limcdif  22823  ellimc2  22824  limcmpt  22830  limcres  22833  plydivex  23242  taylfval  23306  legtrid  24628  legso  24636  lmicom  24822  nb3graprlem2  25172  numclwwlk3lem  25828  atomli  28027  atoml2i  28028  or3di  28093  disjnf  28177  disjex  28198  disjexc  28199  orngsqr  28569  ind1a  28844  esumcvg  28909  voliune  29054  volfiniune  29055  bnj964  29756  dfso2  30395  socnv  30406  soseq  30493  lineunray  30913  bj-dfbi4  31148  bj-nf3  31190  poimirlem18  31916  poimirlem23  31921  poimirlem27  31925  poimirlem31  31929  itg2addnclem2  31952  tsxo1  32337  tsxo2  32338  tsxo3  32339  tsxo4  32340  tsna1  32344  tsna2  32345  tsna3  32346  ts3an1  32350  ts3an2  32351  ts3an3  32352  ts3or1  32353  ts3or2  32354  ts3or3  32355  prtlem90  32391  ifpim123g  36108  ifpor123g  36116  rp-fakeoranass  36122  frege133d  36261  undif3VD  37184  wallispilem3  37793  iccpartgt  38497  nnsum4primeseven  38651  nnsum4primesevenALTV  38652  pr1eqbg  38740  lindslinindsimp2  39600