Theorem orbi2i 926

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 219	. . 3 ⊢ (𝜑 → 𝜓)
3	2	orim2i 924	. 2 ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓))
4	1	biimpri 231	. . 3 ⊢ (𝜓 → 𝜑)
5	4	orim2i 924	. 2 ⊢ ((𝜒 ∨ 𝜓) → (𝜒 ∨ 𝜑))
6	3, 5	impbii 212	1 ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  orbi1i  927  orbi12i  928  orass  935  or4  940  or42  941  orordir  943  dn1  1073  dfifp6  1084  excxor  1546  nf3  1819  19.44v  2033  19.44  2277  sspsstri  4036  unass  4173  undi  4233  undif3  4248  2nreu  4405  undif4  4423  ssunpr  4794  sspr  4795  sstp  4796  pr1eqbg  4817  iinun2  5036  iinuni  5063  qfto  6133  somin1  6145  ordtri2  6424  on0eqel  6514  frxp  8175  poxp2  8197  soseq  8213  frrlem12  8353  supgtoreq  9500  wemapsolem  9581  fin1a2lem12  10528  psslinpr  11155  suplem2pr  11177  fimaxre  12301  ind1a  12371  elnn0  12648  elxnn0  12721  elnn1uz2  13092  elxr  13285  xrinfmss  13480  elfzp1  13748  hashf1lem2  14642  dvdslelem  16523  pythagtrip  17056  tosso  18641  orngsqr  21174  maducoeval2  23010  madugsum  23013  ist0-3  23718  limcdif  26251  ellimc2  26252  limcmpt  26258  limcres  26261  plydivex  26673  taylfval  26743  precsexlem9  28658  z12zsodd  28925  legtrid  29111  legso  29119  lmicom  29350  numedglnl  29779  nb3grprlem2  30019  clwwlkneq0  30677  atomli  33041  atoml2i  33042  or3di  33156  disjnf  33262  disjex  33284  disjexc  33285  cycpmrn  33803  esumcvg  34829  voliune  34973  volfiniune  34974  bnj964  35684  satfvsucsuc  36338  satfrnmapom  36343  satf0op  36350  fmlaomn0  36363  dfso2  36735  lineunray  37127  bj-dfbi4  37658  bj-axadj  38169  wl-ifpimpr  38657  wl-df4-3mintru2  38678  poimirlem18  38824  poimirlem23  38829  poimirlem27  38833  poimirlem31  38837  itg2addnclem2  38858  tsxo1  39335  tsxo2  39336  tsxo3  39337  tsxo4  39338  tsna1  39342  tsna2  39343  tsna3  39344  ts3an1  39348  ts3an2  39349  ts3an3  39350  ts3or1  39351  ts3or2  39352  ts3or3  39353  dfeldisj5  40011  aks4d1p7  43399  reelznn0nn  43791  dflim5  44592  ifpim123g  44762  ifpor123g  44770  rp-fakeoranass  44776  ontric3g  44784  frege133d  45026  or3or  45284  undif3VD  46124  wallispilem3  47350  iccpartgt  48782  nnsum4primeseven  49171  nnsum4primesevenALTV  49172  clnbupgrel  49205  usgrexmpl2trifr  49408  pg4cyclnex  49498  lindslinindsimp2  49906  veronesevrowd  51407