Theorem orbi2i 910

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

Syntax hints:   ↔ wb 205   ∨ wo 844

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 206  df-or 845

This theorem is referenced by:  orbi1i  911  orbi12i  912  orass  919  or4  924  or42  925  orordir  927  dn1  1055  dfifp6  1066  excxor  1512  nf3  1789  nfnbiOLD  1858  19.44v  1996  19.44  2230  sspsstri  4037  unass  4100  undi  4208  undif3  4224  2nreu  4375  undif4  4400  ssunpr  4765  sspr  4766  sstp  4767  pr1eqbg  4787  iinun2  5002  iinuni  5027  qfto  6026  somin1  6038  ordtri2  6301  on0eqel  6384  frxp  7967  frrlem12  8113  wfrlem14OLD  8153  wfrlem15OLD  8154  supgtoreq  9229  wemapsolem  9309  fin1a2lem12  10167  psslinpr  10787  suplem2pr  10809  fimaxre  11919  elnn0  12235  elxnn0  12307  elnn1uz2  12665  elxr  12852  xrinfmss  13044  elfzp1  13306  hashf1lem2  14170  dvdslelem  16018  pythagtrip  16535  tosso  18137  maducoeval2  21789  madugsum  21792  ist0-3  22496  limcdif  25040  ellimc2  25041  limcmpt  25047  limcres  25050  plydivex  25457  taylfval  25518  legtrid  26952  legso  26960  lmicom  27149  numedglnl  27514  nb3grprlem2  27748  clwwlkneq0  28393  atomli  30744  atoml2i  30745  or3di  30810  disjnf  30909  disjex  30931  disjexc  30932  cycpmrn  31410  orngsqr  31503  ind1a  31987  esumcvg  32054  voliune  32197  volfiniune  32198  bnj964  32923  satfvsucsuc  33327  satfrnmapom  33332  satf0op  33339  fmlaomn0  33352  dfso2  33722  poxp2  33790  poxp3  33796  soseq  33803  lineunray  34449  bj-dfbi4  34754  wl-ifpimpr  35637  wl-df4-3mintru2  35658  poimirlem18  35795  poimirlem23  35800  poimirlem27  35804  poimirlem31  35808  itg2addnclem2  35829  tsxo1  36295  tsxo2  36296  tsxo3  36297  tsxo4  36298  tsna1  36302  tsna2  36303  tsna3  36304  ts3an1  36308  ts3an2  36309  ts3an3  36310  ts3or1  36311  ts3or2  36312  ts3or3  36313  dfeldisj5  36832  aks4d1p7  40091  ifpim123g  41107  ifpor123g  41115  rp-fakeoranass  41121  ontric3g  41129  frege133d  41373  or3or  41631  undif3VD  42502  wallispilem3  43608  iccpartgt  44879  nnsum4primeseven  45252  nnsum4primesevenALTV  45253  lindslinindsimp2  45804