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  4068  unass  4135  undi  4248  undif3  4263  2nreu  4407  undif4  4430  ssunpr  4798  sspr  4799  sstp  4800  pr1eqbg  4821  iinun2  5037  iinuni  5062  qfto  6094  somin1  6106  ordtri2  6367  on0eqel  6458  frxp  8105  poxp2  8122  soseq  8138  frrlem12  8276  supgtoreq  9422  wemapsolem  9503  fin1a2lem12  10364  psslinpr  10984  suplem2pr  11006  fimaxre  12127  elnn0  12444  elxnn0  12517  elnn1uz2  12884  elxr  13076  xrinfmss  13270  elfzp1  13535  hashf1lem2  14421  dvdslelem  16279  pythagtrip  16805  tosso  18378  maducoeval2  22527  madugsum  22530  ist0-3  23232  limcdif  25777  ellimc2  25778  limcmpt  25784  limcres  25787  plydivex  26205  taylfval  26266  precsexlem9  28117  legtrid  28518  legso  28526  lmicom  28715  numedglnl  29071  nb3grprlem2  29308  clwwlkneq0  29958  atomli  32311  atoml2i  32312  or3di  32388  disjnf  32499  disjex  32521  disjexc  32522  ind1a  32782  cycpmrn  33100  orngsqr  33282  esumcvg  34076  voliune  34219  volfiniune  34220  bnj964  34933  satfvsucsuc  35352  satfrnmapom  35357  satf0op  35364  fmlaomn0  35377  dfso2  35742  lineunray  36135  bj-dfbi4  36561  bj-axadj  37029  wl-ifpimpr  37454  wl-df4-3mintru2  37475  poimirlem18  37632  poimirlem23  37637  poimirlem27  37641  poimirlem31  37645  itg2addnclem2  37666  tsxo1  38131  tsxo2  38132  tsxo3  38133  tsxo4  38134  tsna1  38138  tsna2  38139  tsna3  38140  ts3an1  38144  ts3an2  38145  ts3an3  38146  ts3or1  38147  ts3or2  38148  ts3or3  38149  dfeldisj5  38713  aks4d1p7  42071  reelznn0nn  42449  dflim5  43318  ifpim123g  43489  ifpor123g  43497  rp-fakeoranass  43503  ontric3g  43511  frege133d  43754  or3or  44012  undif3VD  44871  wallispilem3  46065  iccpartgt  47428  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  clnbupgrel  47835  usgrexmpl2trifr  48028  pg4cyclnex  48117  lindslinindsimp2  48452