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

Syntax hints:   ↔ wb 206   ∨ wo 846

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 847

This theorem is referenced by:  orbi1i  912  orbi12i  913  orass  920  or4  925  or42  926  orordir  928  dn1  1058  dfifp6  1069  excxor  1513  nf3  1784  nfnbiOLD  1854  19.44v  1992  19.44  2238  sspsstri  4128  unass  4195  undi  4304  undif3  4319  2nreu  4467  undif4  4490  ssunpr  4859  sspr  4860  sstp  4861  pr1eqbg  4881  iinun2  5096  iinuni  5121  qfto  6153  somin1  6165  ordtri2  6430  on0eqel  6519  frxp  8167  poxp2  8184  soseq  8200  frrlem12  8338  wfrlem14OLD  8378  wfrlem15OLD  8379  supgtoreq  9539  wemapsolem  9619  fin1a2lem12  10480  psslinpr  11100  suplem2pr  11122  fimaxre  12239  elnn0  12555  elxnn0  12627  elnn1uz2  12990  elxr  13179  xrinfmss  13372  elfzp1  13634  hashf1lem2  14505  dvdslelem  16357  pythagtrip  16881  tosso  18489  maducoeval2  22667  madugsum  22670  ist0-3  23374  limcdif  25931  ellimc2  25932  limcmpt  25938  limcres  25941  plydivex  26357  taylfval  26418  precsexlem9  28257  legtrid  28617  legso  28625  lmicom  28814  numedglnl  29179  nb3grprlem2  29416  clwwlkneq0  30061  atomli  32414  atoml2i  32415  or3di  32488  disjnf  32592  disjex  32614  disjexc  32615  cycpmrn  33136  orngsqr  33299  ind1a  33983  esumcvg  34050  voliune  34193  volfiniune  34194  bnj964  34919  satfvsucsuc  35333  satfrnmapom  35338  satf0op  35345  fmlaomn0  35358  dfso2  35717  lineunray  36111  bj-dfbi4  36539  bj-axadj  37007  wl-ifpimpr  37432  wl-df4-3mintru2  37453  poimirlem18  37598  poimirlem23  37603  poimirlem27  37607  poimirlem31  37611  itg2addnclem2  37632  tsxo1  38097  tsxo2  38098  tsxo3  38099  tsxo4  38100  tsna1  38104  tsna2  38105  tsna3  38106  ts3an1  38110  ts3an2  38111  ts3an3  38112  ts3or1  38113  ts3or2  38114  ts3or3  38115  dfeldisj5  38677  aks4d1p7  42040  reelznn0nn  42425  dflim5  43291  ifpim123g  43462  ifpor123g  43470  rp-fakeoranass  43476  ontric3g  43484  frege133d  43727  or3or  43985  undif3VD  44853  wallispilem3  45988  iccpartgt  47301  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  clnbupgrel  47707  usgrexmpl2trifr  47852  lindslinindsimp2  48192