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  1517  nf3  1787  19.44v  1999  19.44  2242  sspsstri  4055  unass  4122  undi  4235  undif3  4250  2nreu  4394  undif4  4417  ssunpr  4788  sspr  4789  sstp  4790  pr1eqbg  4811  iinun2  5026  iinuni  5051  qfto  6076  somin1  6088  ordtri2  6350  on0eqel  6440  frxp  8066  poxp2  8083  soseq  8099  frrlem12  8237  supgtoreq  9372  wemapsolem  9453  fin1a2lem12  10319  psslinpr  10940  suplem2pr  10962  fimaxre  12084  elnn0  12401  elxnn0  12474  elnn1uz2  12836  elxr  13028  xrinfmss  13223  elfzp1  13488  hashf1lem2  14377  dvdslelem  16234  pythagtrip  16760  tosso  18338  orngsqr  20797  maducoeval2  22582  madugsum  22585  ist0-3  23287  limcdif  25831  ellimc2  25832  limcmpt  25838  limcres  25841  plydivex  26259  taylfval  26320  precsexlem9  28183  zs12zodd  28431  legtrid  28612  legso  28620  lmicom  28809  numedglnl  29166  nb3grprlem2  29403  clwwlkneq0  30053  atomli  32406  atoml2i  32407  or3di  32482  disjnf  32594  disjex  32616  disjexc  32617  ind1a  32887  cycpmrn  33174  esumcvg  34192  voliune  34335  volfiniune  34336  bnj964  35048  satfvsucsuc  35508  satfrnmapom  35513  satf0op  35520  fmlaomn0  35533  dfso2  35898  lineunray  36290  bj-dfbi4  36716  bj-axadj  37185  wl-ifpimpr  37610  wl-df4-3mintru2  37631  poimirlem18  37778  poimirlem23  37783  poimirlem27  37787  poimirlem31  37791  itg2addnclem2  37812  tsxo1  38277  tsxo2  38278  tsxo3  38279  tsxo4  38280  tsna1  38284  tsna2  38285  tsna3  38286  ts3an1  38290  ts3an2  38291  ts3an3  38292  ts3or1  38293  ts3or2  38294  ts3or3  38295  dfeldisj5  38919  aks4d1p7  42276  reelznn0nn  42658  dflim5  43513  ifpim123g  43683  ifpor123g  43691  rp-fakeoranass  43697  ontric3g  43705  frege133d  43948  or3or  44206  undif3VD  45064  wallispilem3  46253  iccpartgt  47615  nnsum4primeseven  47988  nnsum4primesevenALTV  47989  clnbupgrel  48022  usgrexmpl2trifr  48225  pg4cyclnex  48315  lindslinindsimp2  48651