Theorem orbi2i 541

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

Syntax hints:   ↔ wb 196   ∨ wo 383

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 197  df-or 385

This theorem is referenced by:  orbi1i  542  orbi12i  543  orass  546  or4  550  or42  551  orordir  553  dn1  1008  dfifp6  1018  3orcomb  1048  excxor  1469  nf3  1712  19.44v  1912  19.44  2106  r19.30  3082  sspsstri  3709  unass  3770  undi  3874  undif3  3888  undif3OLD  3889  undif4  4035  ssunpr  4365  sspr  4366  sstp  4367  pr1eqbg  4390  iinun2  4586  iinuni  4609  qfto  5517  somin1  5529  ordtri2  5758  on0eqel  5845  frxp  7287  wfrlem14  7428  wfrlem15  7429  supgtoreq  8376  wemapsolem  8455  fin1a2lem12  9233  psslinpr  9853  suplem2pr  9875  fimaxre  10968  elnn0  11294  elxnn0  11365  elnn1uz2  11765  elxr  11950  xrinfmss  12140  elfzp1  12391  hashf1lem2  13240  dvdslelem  15031  pythagtrip  15539  tosso  17036  maducoeval2  20446  madugsum  20449  ist0-3  21149  limcdif  23640  ellimc2  23641  limcmpt  23647  limcres  23650  plydivex  24052  taylfval  24113  legtrid  25486  legso  25494  lmicom  25680  numedglnl  26039  nb3grprlem2  26283  numclwwlk3lem  27241  atomli  29241  atoml2i  29242  or3di  29307  disjnf  29384  disjex  29405  disjexc  29406  orngsqr  29804  ind1a  30081  esumcvg  30148  voliune  30292  volfiniune  30293  bnj964  31013  dfso2  31644  soseq  31751  lineunray  32254  bj-dfbi4  32558  poimirlem18  33427  poimirlem23  33432  poimirlem27  33436  poimirlem31  33440  itg2addnclem2  33462  tsxo1  33944  tsxo2  33945  tsxo3  33946  tsxo4  33947  tsna1  33951  tsna2  33952  tsna3  33953  ts3an1  33957  ts3an2  33958  ts3an3  33959  ts3or1  33960  ts3or2  33961  ts3or3  33962  ifpim123g  37845  ifpor123g  37853  rp-fakeoranass  37859  frege133d  38057  or3or  38319  undif3VD  39118  wallispilem3  40284  iccpartgt  41363  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  lindslinindsimp2  42252