Theorem orbi2i 926

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

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  orbi1i  927  orbi12i  928  orass  935  or4  940  or42  941  orordir  943  dn1  1073  dfifp6  1084  excxor  1546  nf3  1819  19.44v  2031  19.44  2273  sspsstri  4054  unass  4118  undi  4231  undif3  4246  2nreu  4402  undif4  4420  ssunpr  4794  sspr  4795  sstp  4796  pr1eqbg  4817  iinun2  5031  iinuni  5058  qfto  6115  somin1  6127  ordtri2  6393  on0eqel  6483  frxp  8124  poxp2  8141  soseq  8157  frrlem12  8296  supgtoreq  9441  wemapsolem  9522  fin1a2lem12  10413  psslinpr  11040  suplem2pr  11062  fimaxre  12183  ind1a  12253  elnn0  12530  elxnn0  12603  elnn1uz2  12974  elxr  13167  xrinfmss  13362  elfzp1  13629  hashf1lem2  14521  dvdslelem  16399  pythagtrip  16926  tosso  18505  orngsqr  21032  maducoeval2  22862  madugsum  22865  ist0-3  23570  limcdif  26103  ellimc2  26104  limcmpt  26110  limcres  26113  plydivex  26527  taylfval  26595  precsexlem9  28480  z12zsodd  28747  legtrid  28933  legso  28941  lmicom  29172  numedglnl  29601  nb3grprlem2  29841  clwwlkneq0  30499  atomli  32863  atoml2i  32864  or3di  32936  disjnf  33043  disjex  33065  disjexc  33066  cycpmrn  33583  esumcvg  34596  voliune  34740  volfiniune  34741  bnj964  35452  satfvsucsuc  35944  satfrnmapom  35949  satf0op  35956  fmlaomn0  35969  dfso2  36334  lineunray  36727  bj-dfbi4  37274  bj-axadj  37785  wl-ifpimpr  38220  wl-df4-3mintru2  38241  poimirlem18  38387  poimirlem23  38392  poimirlem27  38396  poimirlem31  38400  itg2addnclem2  38421  tsxo1  38885  tsxo2  38886  tsxo3  38887  tsxo4  38888  tsna1  38892  tsna2  38893  tsna3  38894  ts3an1  38898  ts3an2  38899  ts3an3  38900  ts3or1  38901  ts3or2  38902  ts3or3  38903  dfeldisj5  39561  aks4d1p7  42949  reelznn0nn  43349  dflim5  44170  ifpim123g  44340  ifpor123g  44348  rp-fakeoranass  44354  ontric3g  44362  frege133d  44605  or3or  44863  undif3VD  45704  wallispilem3  46895  iccpartgt  48327  nnsum4primeseven  48716  nnsum4primesevenALTV  48717  clnbupgrel  48750  usgrexmpl2trifr  48953  pg4cyclnex  49043  lindslinindsimp2  49393  veronesevrowd  50812