Theorem orbi2i 912

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

Syntax hints:   ↔ wb 206   ∨ wo 847

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 848

This theorem is referenced by:  orbi1i  913  orbi12i  914  orass  921  or4  926  or42  927  orordir  929  dn1  1057  dfifp6  1068  excxor  1516  nf3  1786  19.44v  1998  19.44  2238  sspsstri  4064  unass  4131  undi  4244  undif3  4259  2nreu  4403  undif4  4426  ssunpr  4794  sspr  4795  sstp  4796  pr1eqbg  4817  iinun2  5032  iinuni  5057  qfto  6082  somin1  6094  ordtri2  6355  on0eqel  6446  frxp  8082  poxp2  8099  soseq  8115  frrlem12  8253  supgtoreq  9398  wemapsolem  9479  fin1a2lem12  10340  psslinpr  10960  suplem2pr  10982  fimaxre  12103  elnn0  12420  elxnn0  12493  elnn1uz2  12860  elxr  13052  xrinfmss  13246  elfzp1  13511  hashf1lem2  14397  dvdslelem  16255  pythagtrip  16781  tosso  18358  orngsqr  20786  maducoeval2  22560  madugsum  22563  ist0-3  23265  limcdif  25810  ellimc2  25811  limcmpt  25817  limcres  25820  plydivex  26238  taylfval  26299  precsexlem9  28157  zs12zodd  28394  legtrid  28571  legso  28579  lmicom  28768  numedglnl  29124  nb3grprlem2  29361  clwwlkneq0  30008  atomli  32361  atoml2i  32362  or3di  32438  disjnf  32549  disjex  32571  disjexc  32572  ind1a  32832  cycpmrn  33115  esumcvg  34069  voliune  34212  volfiniune  34213  bnj964  34926  satfvsucsuc  35345  satfrnmapom  35350  satf0op  35357  fmlaomn0  35370  dfso2  35735  lineunray  36128  bj-dfbi4  36554  bj-axadj  37022  wl-ifpimpr  37447  wl-df4-3mintru2  37468  poimirlem18  37625  poimirlem23  37630  poimirlem27  37634  poimirlem31  37638  itg2addnclem2  37659  tsxo1  38124  tsxo2  38125  tsxo3  38126  tsxo4  38127  tsna1  38131  tsna2  38132  tsna3  38133  ts3an1  38137  ts3an2  38138  ts3an3  38139  ts3or1  38140  ts3or2  38141  ts3or3  38142  dfeldisj5  38706  aks4d1p7  42064  reelznn0nn  42442  dflim5  43311  ifpim123g  43482  ifpor123g  43490  rp-fakeoranass  43496  ontric3g  43504  frege133d  43747  or3or  44005  undif3VD  44864  wallispilem3  46058  iccpartgt  47421  nnsum4primeseven  47794  nnsum4primesevenALTV  47795  clnbupgrel  47828  usgrexmpl2trifr  48021  pg4cyclnex  48110  lindslinindsimp2  48445