Theorem orbi2i 912

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 216	. . 3 ⊢ (𝜑 → 𝜓)
3	2	orim2i 910	. 2 ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓))
4	1	biimpri 228	. . 3 ⊢ (𝜓 → 𝜑)
5	4	orim2i 910	. 2 ⊢ ((𝜒 ∨ 𝜓) → (𝜒 ∨ 𝜑))
6	3, 5	impbii 209	1 ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))

Syntax hints:   ↔ wb 206   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  orbi1i  913  orbi12i  914  orass  921  or4  926  or42  927  orordir  929  dn1  1057  dfifp6  1068  excxor  1512  nf3  1782  nfnbiOLD  1852  19.44v  1989  19.44  2234  sspsstri  4114  unass  4181  undi  4290  undif3  4305  2nreu  4449  undif4  4472  ssunpr  4838  sspr  4839  sstp  4840  pr1eqbg  4861  iinun2  5077  iinuni  5102  qfto  6143  somin1  6155  ordtri2  6420  on0eqel  6509  frxp  8149  poxp2  8166  soseq  8182  frrlem12  8320  wfrlem14OLD  8360  wfrlem15OLD  8361  supgtoreq  9507  wemapsolem  9587  fin1a2lem12  10448  psslinpr  11068  suplem2pr  11090  fimaxre  12209  elnn0  12525  elxnn0  12598  elnn1uz2  12964  elxr  13155  xrinfmss  13348  elfzp1  13610  hashf1lem2  14491  dvdslelem  16342  pythagtrip  16867  tosso  18476  maducoeval2  22661  madugsum  22664  ist0-3  23368  limcdif  25925  ellimc2  25926  limcmpt  25932  limcres  25935  plydivex  26353  taylfval  26414  precsexlem9  28253  legtrid  28613  legso  28621  lmicom  28810  numedglnl  29175  nb3grprlem2  29412  clwwlkneq0  30057  atomli  32410  atoml2i  32411  or3di  32487  disjnf  32589  disjex  32611  disjexc  32612  cycpmrn  33145  orngsqr  33313  ind1a  33999  esumcvg  34066  voliune  34209  volfiniune  34210  bnj964  34935  satfvsucsuc  35349  satfrnmapom  35354  satf0op  35361  fmlaomn0  35374  dfso2  35734  lineunray  36128  bj-dfbi4  36555  bj-axadj  37023  wl-ifpimpr  37448  wl-df4-3mintru2  37469  poimirlem18  37624  poimirlem23  37629  poimirlem27  37633  poimirlem31  37637  itg2addnclem2  37658  tsxo1  38123  tsxo2  38124  tsxo3  38125  tsxo4  38126  tsna1  38130  tsna2  38131  tsna3  38132  ts3an1  38136  ts3an2  38137  ts3an3  38138  ts3or1  38139  ts3or2  38140  ts3or3  38141  dfeldisj5  38702  aks4d1p7  42064  reelznn0nn  42455  dflim5  43318  ifpim123g  43489  ifpor123g  43497  rp-fakeoranass  43503  ontric3g  43511  frege133d  43754  or3or  44012  undif3VD  44879  wallispilem3  46022  iccpartgt  47351  nnsum4primeseven  47724  nnsum4primesevenALTV  47725  clnbupgrel  47758  usgrexmpl2trifr  47931  lindslinindsimp2  48308