Theorem orbi2i 925

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

Syntax hints:   ↔ wb 209   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  orbi1i  926  orbi12i  927  orass  934  or4  939  or42  940  orordir  942  dn1  1071  dfifp6  1082  excxor  1543  nf3  1813  19.44v  2025  19.44  2279  sspsstri  4068  unass  4133  undi  4246  undif3  4261  2nreu  4415  undif4  4433  ssunpr  4803  sspr  4804  sstp  4805  pr1eqbg  4826  iinun2  5041  iinuni  5068  qfto  6122  somin1  6134  ordtri2  6397  on0eqel  6487  frxp  8121  poxp2  8138  soseq  8154  frrlem12  8293  supgtoreq  9430  wemapsolem  9511  fin1a2lem12  10394  psslinpr  11015  suplem2pr  11037  fimaxre  12158  ind1a  12228  elnn0  12505  elxnn0  12578  elnn1uz2  12948  elxr  13140  xrinfmss  13335  elfzp1  13601  hashf1lem2  14492  dvdslelem  16366  pythagtrip  16893  tosso  18472  orngsqr  20946  maducoeval2  22765  madugsum  22768  ist0-3  23470  limcdif  26003  ellimc2  26004  limcmpt  26010  limcres  26013  plydivex  26426  taylfval  26487  precsexlem9  28373  z12zsodd  28640  legtrid  28825  legso  28833  lmicom  29054  numedglnl  29434  nb3grprlem2  29671  clwwlkneq0  30320  atomli  32674  atoml2i  32675  or3di  32747  disjnf  32855  disjex  32877  disjexc  32878  cycpmrn  33403  esumcvg  34420  voliune  34563  volfiniune  34564  bnj964  35275  satfvsucsuc  35755  satfrnmapom  35760  satf0op  35767  fmlaomn0  35780  dfso2  36145  lineunray  36537  bj-dfbi4  37054  bj-axadj  37564  wl-ifpimpr  37999  wl-df4-3mintru2  38020  poimirlem18  38176  poimirlem23  38181  poimirlem27  38185  poimirlem31  38189  itg2addnclem2  38210  tsxo1  38675  tsxo2  38676  tsxo3  38677  tsxo4  38678  tsna1  38682  tsna2  38683  tsna3  38684  ts3an1  38688  ts3an2  38689  ts3an3  38690  ts3or1  38691  ts3or2  38692  ts3or3  38693  dfeldisj5  39351  aks4d1p7  42739  reelznn0nn  43124  dflim5  43947  ifpim123g  44117  ifpor123g  44125  rp-fakeoranass  44131  ontric3g  44139  frege133d  44382  or3or  44640  undif3VD  45481  wallispilem3  46672  iccpartgt  48064  nnsum4primeseven  48453  nnsum4primesevenALTV  48454  clnbupgrel  48487  usgrexmpl2trifr  48690  pg4cyclnex  48780  lindslinindsimp2  49127