Theorem orbi2i 913

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

Syntax hints:   ↔ wb 206   ∨ wo 848

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 849

This theorem is referenced by:  orbi1i  914  orbi12i  915  orass  922  or4  927  or42  928  orordir  930  dn1  1058  dfifp6  1069  excxor  1518  nf3  1788  19.44v  2000  19.44  2245  sspsstri  4045  unass  4112  undi  4225  undif3  4240  2nreu  4384  undif4  4407  ssunpr  4777  sspr  4778  sstp  4779  pr1eqbg  4800  iinun2  5015  iinuni  5040  qfto  6084  somin1  6096  ordtri2  6358  on0eqel  6448  frxp  8076  poxp2  8093  soseq  8109  frrlem12  8247  supgtoreq  9384  wemapsolem  9465  fin1a2lem12  10333  psslinpr  10954  suplem2pr  10976  fimaxre  12100  ind1a  12170  elnn0  12439  elxnn0  12512  elnn1uz2  12875  elxr  13067  xrinfmss  13262  elfzp1  13528  hashf1lem2  14418  dvdslelem  16278  pythagtrip  16805  tosso  18383  orngsqr  20843  maducoeval2  22605  madugsum  22608  ist0-3  23310  limcdif  25843  ellimc2  25844  limcmpt  25850  limcres  25853  plydivex  26263  taylfval  26324  precsexlem9  28207  z12zsodd  28474  legtrid  28659  legso  28667  lmicom  28856  numedglnl  29213  nb3grprlem2  29450  clwwlkneq0  30099  atomli  32453  atoml2i  32454  or3di  32528  disjnf  32640  disjex  32662  disjexc  32663  cycpmrn  33204  esumcvg  34230  voliune  34373  volfiniune  34374  bnj964  35085  satfvsucsuc  35547  satfrnmapom  35552  satf0op  35559  fmlaomn0  35572  dfso2  35937  lineunray  36329  bj-dfbi4  36838  bj-axadj  37348  wl-ifpimpr  37782  wl-df4-3mintru2  37803  poimirlem18  37959  poimirlem23  37964  poimirlem27  37968  poimirlem31  37972  itg2addnclem2  37993  tsxo1  38458  tsxo2  38459  tsxo3  38460  tsxo4  38461  tsna1  38465  tsna2  38466  tsna3  38467  ts3an1  38471  ts3an2  38472  ts3an3  38473  ts3or1  38474  ts3or2  38475  ts3or3  38476  dfeldisj5  39134  aks4d1p7  42522  reelznn0nn  42906  dflim5  43757  ifpim123g  43927  ifpor123g  43935  rp-fakeoranass  43941  ontric3g  43949  frege133d  44192  or3or  44450  undif3VD  45308  wallispilem3  46495  iccpartgt  47887  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  clnbupgrel  48310  usgrexmpl2trifr  48513  pg4cyclnex  48603  lindslinindsimp2  48939