Theorem orbi2i 911

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

Syntax hints:   ↔ wb 205   ∨ wo 845

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 846

This theorem is referenced by:  orbi1i  912  orbi12i  913  orass  920  or4  925  or42  926  orordir  928  dn1  1056  dfifp6  1067  excxor  1515  nf3  1788  nfnbiOLD  1858  19.44v  1996  19.44  2230  sspsstri  4067  unass  4131  undi  4239  undif3  4255  2nreu  4406  undif4  4431  ssunpr  4797  sspr  4798  sstp  4799  pr1eqbg  4819  iinun2  5038  iinuni  5063  qfto  6080  somin1  6092  ordtri2  6357  on0eqel  6446  frxp  8063  poxp2  8080  soseq  8096  frrlem12  8233  wfrlem14OLD  8273  wfrlem15OLD  8274  supgtoreq  9415  wemapsolem  9495  fin1a2lem12  10356  psslinpr  10976  suplem2pr  10998  fimaxre  12108  elnn0  12424  elxnn0  12496  elnn1uz2  12859  elxr  13046  xrinfmss  13239  elfzp1  13501  hashf1lem2  14367  dvdslelem  16202  pythagtrip  16717  tosso  18322  maducoeval2  22026  madugsum  22029  ist0-3  22733  limcdif  25277  ellimc2  25278  limcmpt  25284  limcres  25287  plydivex  25694  taylfval  25755  legtrid  27596  legso  27604  lmicom  27793  numedglnl  28158  nb3grprlem2  28392  clwwlkneq0  29036  atomli  31387  atoml2i  31388  or3di  31453  disjnf  31555  disjex  31577  disjexc  31578  cycpmrn  32062  orngsqr  32170  ind1a  32707  esumcvg  32774  voliune  32917  volfiniune  32918  bnj964  33644  satfvsucsuc  34046  satfrnmapom  34051  satf0op  34058  fmlaomn0  34071  dfso2  34414  lineunray  34808  bj-dfbi4  35113  bj-axadj  35585  wl-ifpimpr  36010  wl-df4-3mintru2  36031  poimirlem18  36169  poimirlem23  36174  poimirlem27  36178  poimirlem31  36182  itg2addnclem2  36203  tsxo1  36669  tsxo2  36670  tsxo3  36671  tsxo4  36672  tsna1  36676  tsna2  36677  tsna3  36678  ts3an1  36682  ts3an2  36683  ts3an3  36684  ts3or1  36685  ts3or2  36686  ts3or3  36687  dfeldisj5  37256  aks4d1p7  40613  reelznn0nn  40976  dflim5  41722  ifpim123g  41894  ifpor123g  41902  rp-fakeoranass  41908  ontric3g  41916  frege133d  42159  or3or  42417  undif3VD  43286  wallispilem3  44428  iccpartgt  45739  nnsum4primeseven  46112  nnsum4primesevenALTV  46113  lindslinindsimp2  46664