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  4071  unass  4138  undi  4251  undif3  4266  2nreu  4410  undif4  4433  ssunpr  4801  sspr  4802  sstp  4803  pr1eqbg  4824  iinun2  5040  iinuni  5065  qfto  6097  somin1  6109  ordtri2  6370  on0eqel  6461  frxp  8108  poxp2  8125  soseq  8141  frrlem12  8279  supgtoreq  9429  wemapsolem  9510  fin1a2lem12  10371  psslinpr  10991  suplem2pr  11013  fimaxre  12134  elnn0  12451  elxnn0  12524  elnn1uz2  12891  elxr  13083  xrinfmss  13277  elfzp1  13542  hashf1lem2  14428  dvdslelem  16286  pythagtrip  16812  tosso  18385  maducoeval2  22534  madugsum  22537  ist0-3  23239  limcdif  25784  ellimc2  25785  limcmpt  25791  limcres  25794  plydivex  26212  taylfval  26273  precsexlem9  28124  legtrid  28525  legso  28533  lmicom  28722  numedglnl  29078  nb3grprlem2  29315  clwwlkneq0  29965  atomli  32318  atoml2i  32319  or3di  32395  disjnf  32506  disjex  32528  disjexc  32529  ind1a  32789  cycpmrn  33107  orngsqr  33289  esumcvg  34083  voliune  34226  volfiniune  34227  bnj964  34940  satfvsucsuc  35359  satfrnmapom  35364  satf0op  35371  fmlaomn0  35384  dfso2  35749  lineunray  36142  bj-dfbi4  36568  bj-axadj  37036  wl-ifpimpr  37461  wl-df4-3mintru2  37482  poimirlem18  37639  poimirlem23  37644  poimirlem27  37648  poimirlem31  37652  itg2addnclem2  37673  tsxo1  38138  tsxo2  38139  tsxo3  38140  tsxo4  38141  tsna1  38145  tsna2  38146  tsna3  38147  ts3an1  38151  ts3an2  38152  ts3an3  38153  ts3or1  38154  ts3or2  38155  ts3or3  38156  dfeldisj5  38720  aks4d1p7  42078  reelznn0nn  42456  dflim5  43325  ifpim123g  43496  ifpor123g  43504  rp-fakeoranass  43510  ontric3g  43518  frege133d  43761  or3or  44019  undif3VD  44878  wallispilem3  46072  iccpartgt  47432  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  clnbupgrel  47839  usgrexmpl2trifr  48032  pg4cyclnex  48121  lindslinindsimp2  48456