Theorem orbi2i 913

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

Syntax hints:   ↔ wb 206   ∨ wo 848

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 849

This theorem is referenced by:  orbi1i  914  orbi12i  915  orass  922  or4  927  or42  928  orordir  930  dn1  1058  dfifp6  1069  excxor  1516  nf3  1786  19.44v  1992  19.44  2237  sspsstri  4105  unass  4172  undi  4285  undif3  4300  2nreu  4444  undif4  4467  ssunpr  4834  sspr  4835  sstp  4836  pr1eqbg  4857  iinun2  5073  iinuni  5098  qfto  6141  somin1  6153  ordtri2  6419  on0eqel  6508  frxp  8151  poxp2  8168  soseq  8184  frrlem12  8322  wfrlem14OLD  8362  wfrlem15OLD  8363  supgtoreq  9510  wemapsolem  9590  fin1a2lem12  10451  psslinpr  11071  suplem2pr  11093  fimaxre  12212  elnn0  12528  elxnn0  12601  elnn1uz2  12967  elxr  13158  xrinfmss  13352  elfzp1  13614  hashf1lem2  14495  dvdslelem  16346  pythagtrip  16872  tosso  18464  maducoeval2  22646  madugsum  22649  ist0-3  23353  limcdif  25911  ellimc2  25912  limcmpt  25918  limcres  25921  plydivex  26339  taylfval  26400  precsexlem9  28239  legtrid  28599  legso  28607  lmicom  28796  numedglnl  29161  nb3grprlem2  29398  clwwlkneq0  30048  atomli  32401  atoml2i  32402  or3di  32478  disjnf  32583  disjex  32605  disjexc  32606  ind1a  32844  cycpmrn  33163  orngsqr  33334  esumcvg  34087  voliune  34230  volfiniune  34231  bnj964  34957  satfvsucsuc  35370  satfrnmapom  35375  satf0op  35382  fmlaomn0  35395  dfso2  35755  lineunray  36148  bj-dfbi4  36574  bj-axadj  37042  wl-ifpimpr  37467  wl-df4-3mintru2  37488  poimirlem18  37645  poimirlem23  37650  poimirlem27  37654  poimirlem31  37658  itg2addnclem2  37679  tsxo1  38144  tsxo2  38145  tsxo3  38146  tsxo4  38147  tsna1  38151  tsna2  38152  tsna3  38153  ts3an1  38157  ts3an2  38158  ts3an3  38159  ts3or1  38160  ts3or2  38161  ts3or3  38162  dfeldisj5  38722  aks4d1p7  42084  reelznn0nn  42479  dflim5  43342  ifpim123g  43513  ifpor123g  43521  rp-fakeoranass  43527  ontric3g  43535  frege133d  43778  or3or  44036  undif3VD  44902  wallispilem3  46082  iccpartgt  47414  nnsum4primeseven  47787  nnsum4primesevenALTV  47788  clnbupgrel  47821  usgrexmpl2trifr  47996  lindslinindsimp2  48380