Theorem orbi2i 918

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

Syntax hints:   ↔ wb 207   ∨ wo 853

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 208  df-or 854

This theorem is referenced by:  orbi1i  919  orbi12i  920  orass  927  or4  932  or42  933  orordir  935  dn1  1063  dfifp6  1074  excxor  1523  nf3  1793  19.44v  2005  19.44  2249  sspsstri  4036  unass  4101  undi  4213  undif3  4228  2nreu  4372  undif4  4395  ssunpr  4765  sspr  4766  sstp  4767  pr1eqbg  4788  iinun2  5002  iinuni  5027  qfto  6071  somin1  6083  ordtri2  6345  on0eqel  6435  frxp  8066  poxp2  8083  soseq  8099  frrlem12  8237  supgtoreq  9374  wemapsolem  9455  fin1a2lem12  10324  psslinpr  10945  suplem2pr  10967  fimaxre  12091  ind1a  12161  elnn0  12430  elxnn0  12503  elnn1uz2  12866  elxr  13058  xrinfmss  13253  elfzp1  13519  hashf1lem2  14409  dvdslelem  16269  pythagtrip  16796  tosso  18374  orngsqr  20838  maducoeval2  22623  madugsum  22626  ist0-3  23328  limcdif  25861  ellimc2  25862  limcmpt  25868  limcres  25871  plydivex  26281  taylfval  26342  precsexlem9  28225  z12zsodd  28492  legtrid  28677  legso  28685  lmicom  28874  numedglnl  29231  nb3grprlem2  29468  clwwlkneq0  30117  atomli  32471  atoml2i  32472  or3di  32546  disjnf  32659  disjex  32681  disjexc  32682  cycpmrn  33224  esumcvg  34270  voliune  34413  volfiniune  34414  bnj964  35125  satfvsucsuc  35593  satfrnmapom  35598  satf0op  35605  fmlaomn0  35618  dfso2  35983  lineunray  36375  bj-dfbi4  36884  bj-axadj  37394  wl-ifpimpr  37828  wl-df4-3mintru2  37849  poimirlem18  38005  poimirlem23  38010  poimirlem27  38014  poimirlem31  38018  itg2addnclem2  38039  tsxo1  38504  tsxo2  38505  tsxo3  38506  tsxo4  38507  tsna1  38511  tsna2  38512  tsna3  38513  ts3an1  38517  ts3an2  38518  ts3an3  38519  ts3or1  38520  ts3or2  38521  ts3or3  38522  dfeldisj5  39180  aks4d1p7  42568  reelznn0nn  42951  dflim5  43774  ifpim123g  43944  ifpor123g  43952  rp-fakeoranass  43958  ontric3g  43966  frege133d  44209  or3or  44467  undif3VD  45325  wallispilem3  46510  iccpartgt  47902  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  clnbupgrel  48325  usgrexmpl2trifr  48528  pg4cyclnex  48618  lindslinindsimp2  48954