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  1539  nf3  1809  19.44v  2021  19.44  2275  sspsstri  4062  unass  4127  undi  4240  undif3  4255  2nreu  4401  undif4  4424  ssunpr  4794  sspr  4795  sstp  4796  pr1eqbg  4817  iinun2  5032  iinuni  5059  qfto  6111  somin1  6123  ordtri2  6385  on0eqel  6475  frxp  8110  poxp2  8127  soseq  8143  frrlem12  8282  supgtoreq  9419  wemapsolem  9500  fin1a2lem12  10383  psslinpr  11004  suplem2pr  11026  fimaxre  12147  ind1a  12217  elnn0  12494  elxnn0  12567  elnn1uz2  12937  elxr  13129  xrinfmss  13324  elfzp1  13590  hashf1lem2  14481  dvdslelem  16355  pythagtrip  16882  tosso  18461  orngsqr  20935  maducoeval2  22754  madugsum  22757  ist0-3  23459  limcdif  25992  ellimc2  25993  limcmpt  25999  limcres  26002  plydivex  26415  taylfval  26476  precsexlem9  28362  z12zsodd  28629  legtrid  28814  legso  28822  lmicom  29036  numedglnl  29399  nb3grprlem2  29636  clwwlkneq0  30285  atomli  32639  atoml2i  32640  or3di  32712  disjnf  32821  disjex  32843  disjexc  32844  cycpmrn  33371  esumcvg  34388  voliune  34531  volfiniune  34532  bnj964  35243  satfvsucsuc  35723  satfrnmapom  35728  satf0op  35735  fmlaomn0  35748  dfso2  36113  lineunray  36505  bj-dfbi4  37023  bj-axadj  37533  wl-ifpimpr  37967  wl-df4-3mintru2  37988  poimirlem18  38144  poimirlem23  38149  poimirlem27  38153  poimirlem31  38157  itg2addnclem2  38178  tsxo1  38643  tsxo2  38644  tsxo3  38645  tsxo4  38646  tsna1  38650  tsna2  38651  tsna3  38652  ts3an1  38656  ts3an2  38657  ts3an3  38658  ts3or1  38659  ts3or2  38660  ts3or3  38661  dfeldisj5  39319  aks4d1p7  42707  reelznn0nn  43090  dflim5  43913  ifpim123g  44083  ifpor123g  44091  rp-fakeoranass  44097  ontric3g  44105  frege133d  44348  or3or  44606  undif3VD  45449  wallispilem3  46640  iccpartgt  48032  nnsum4primeseven  48421  nnsum4primesevenALTV  48422  clnbupgrel  48455  usgrexmpl2trifr  48658  pg4cyclnex  48748  lindslinindsimp2  49095