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

Syntax hints:   ↔ wb 196   ∨ 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 197  df-or 384

This theorem is referenced by:  orbi1i  541  orbi12i  542  orass  545  or4  549  or42  550  orordir  552  dn1  1028  dfifp6  1038  3orcombOLD  1066  excxor  1509  nf3  1752  19.44v  1968  19.44  2144  r19.30  3111  sspsstri  3742  unass  3803  undi  3907  undif3  3921  undif3OLD  3922  undif4  4068  ssunpr  4397  sspr  4398  sstp  4399  pr1eqbg  4421  iinun2  4618  iinuni  4641  qfto  5552  somin1  5564  ordtri2  5796  on0eqel  5883  frxp  7332  wfrlem14  7473  wfrlem15  7474  supgtoreq  8417  wemapsolem  8496  fin1a2lem12  9271  psslinpr  9891  suplem2pr  9913  fimaxre  11006  elnn0  11332  elxnn0  11403  elnn1uz2  11803  elxr  11988  xrinfmss  12178  elfzp1  12429  hashf1lem2  13278  dvdslelem  15078  pythagtrip  15586  tosso  17083  maducoeval2  20494  madugsum  20497  ist0-3  21197  limcdif  23685  ellimc2  23686  limcmpt  23692  limcres  23695  plydivex  24097  taylfval  24158  legtrid  25531  legso  25539  lmicom  25725  numedglnl  26084  nb3grprlem2  26327  clwwlkneq0  26990  numclwwlk3lemOLD  27369  atomli  29369  atoml2i  29370  or3di  29435  disjnf  29510  disjex  29531  disjexc  29532  orngsqr  29932  ind1a  30209  esumcvg  30276  voliune  30420  volfiniune  30421  bnj964  31139  dfso2  31770  soseq  31879  lineunray  32379  bj-dfbi4  32683  poimirlem18  33557  poimirlem23  33562  poimirlem27  33566  poimirlem31  33570  itg2addnclem2  33592  tsxo1  34074  tsxo2  34075  tsxo3  34076  tsxo4  34077  tsna1  34081  tsna2  34082  tsna3  34083  ts3an1  34087  ts3an2  34088  ts3an3  34089  ts3or1  34090  ts3or2  34091  ts3or3  34092  ifpim123g  38162  ifpor123g  38170  rp-fakeoranass  38176  frege133d  38374  or3or  38636  undif3VD  39432  wallispilem3  40602  iccpartgt  41688  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  lindslinindsimp2  42577