Theorem orbi2i 540

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

Syntax hints:   ↔ wb 195   ∨ wo 382

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 196  df-or 384

This theorem is referenced by:  orbi1i  541  orbi12i  542  orass  545  or4  549  or42  550  orordir  552  dn1  1000  dfifp6  1012  3orcomb  1041  excxor  1461  nf3  1703  19.44v  1899  19.44  2093  r19.30  3063  sspsstri  3671  unass  3732  undi  3833  undif3  3847  undif3OLD  3848  undif4  3987  ssunpr  4305  sspr  4306  sstp  4307  iinun2  4522  iinuni  4545  qfto  5436  somin1  5448  ordtri2  5675  on0eqel  5762  frxp  7174  wfrlem14  7315  wfrlem15  7316  supgtoreq  8259  wemapsolem  8338  fin1a2lem12  9116  psslinpr  9732  suplem2pr  9754  fimaxre  10847  elnn0  11171  elxnn0  11242  elnn1uz2  11641  elxr  11826  xrinfmss  12012  elfzp1  12261  hashf1lem2  13097  dvdslelem  14869  pythagtrip  15377  tosso  16859  maducoeval2  20265  madugsum  20268  ist0-3  20959  limcdif  23446  ellimc2  23447  limcmpt  23453  limcres  23456  plydivex  23856  taylfval  23917  legtrid  25286  legso  25294  lmicom  25480  nb3graprlem2  25981  numclwwlk3lem  26635  atomli  28625  atoml2i  28626  or3di  28691  disjnf  28766  disjex  28787  disjexc  28788  orngsqr  29135  ind1a  29410  esumcvg  29475  voliune  29619  volfiniune  29620  bnj964  30267  dfso2  30897  socnv  30908  soseq  30995  lineunray  31424  bj-dfbi4  31728  bj-nf3  31767  poimirlem18  32597  poimirlem23  32602  poimirlem27  32606  poimirlem31  32610  itg2addnclem2  32632  tsxo1  33114  tsxo2  33115  tsxo3  33116  tsxo4  33117  tsna1  33121  tsna2  33122  tsna3  33123  ts3an1  33127  ts3an2  33128  ts3an3  33129  ts3or1  33130  ts3or2  33131  ts3or3  33132  ifpim123g  36864  ifpor123g  36872  rp-fakeoranass  36878  frege133d  37076  or3or  37339  undif3VD  38140  wallispilem3  38960  iccpartgt  39965  nnsum4primeseven  40216  nnsum4primesevenALTV  40217  pr1eqbg  40313  nb3grprlem2  40609  av-numclwwlk3lem  41538  lindslinindsimp2  42046