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 215	. . 3 ⊢ (𝜑 → 𝜓)
3	2	orim2i 910	. 2 ⊢ ((𝜒 ∨ 𝜑) → (𝜒 ∨ 𝜓))
4	1	biimpri 227	. . 3 ⊢ (𝜓 → 𝜑)
5	4	orim2i 910	. 2 ⊢ ((𝜒 ∨ 𝜓) → (𝜒 ∨ 𝜑))
6	3, 5	impbii 208	1 ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))

Syntax hints:   ↔ wb 205   ∨ wo 846

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 206  df-or 847

This theorem is referenced by:  orbi1i  913  orbi12i  914  orass  921  or4  926  or42  927  orordir  929  dn1  1057  dfifp6  1068  excxor  1516  nf3  1789  nfnbiOLD  1859  19.44v  1997  19.44  2231  sspsstri  4100  unass  4164  undi  4272  undif3  4288  2nreu  4439  undif4  4464  ssunpr  4833  sspr  4834  sstp  4835  pr1eqbg  4855  iinun2  5074  iinuni  5099  qfto  6118  somin1  6130  ordtri2  6395  on0eqel  6484  frxp  8106  poxp2  8123  soseq  8139  frrlem12  8276  wfrlem14OLD  8316  wfrlem15OLD  8317  supgtoreq  9460  wemapsolem  9540  fin1a2lem12  10401  psslinpr  11021  suplem2pr  11043  fimaxre  12153  elnn0  12469  elxnn0  12541  elnn1uz2  12904  elxr  13091  xrinfmss  13284  elfzp1  13546  hashf1lem2  14412  dvdslelem  16247  pythagtrip  16762  tosso  18367  maducoeval2  22123  madugsum  22126  ist0-3  22830  limcdif  25374  ellimc2  25375  limcmpt  25381  limcres  25384  plydivex  25791  taylfval  25852  precsexlem9  27640  legtrid  27821  legso  27829  lmicom  28018  numedglnl  28383  nb3grprlem2  28617  clwwlkneq0  29261  atomli  31612  atoml2i  31613  or3di  31678  disjnf  31778  disjex  31800  disjexc  31801  cycpmrn  32279  orngsqr  32390  ind1a  32954  esumcvg  33021  voliune  33164  volfiniune  33165  bnj964  33891  satfvsucsuc  34293  satfrnmapom  34298  satf0op  34305  fmlaomn0  34318  dfso2  34662  lineunray  35056  bj-dfbi4  35387  bj-axadj  35859  wl-ifpimpr  36284  wl-df4-3mintru2  36305  poimirlem18  36443  poimirlem23  36448  poimirlem27  36452  poimirlem31  36456  itg2addnclem2  36477  tsxo1  36942  tsxo2  36943  tsxo3  36944  tsxo4  36945  tsna1  36949  tsna2  36950  tsna3  36951  ts3an1  36955  ts3an2  36956  ts3an3  36957  ts3or1  36958  ts3or2  36959  ts3or3  36960  dfeldisj5  37528  aks4d1p7  40885  reelznn0nn  41265  dflim5  42011  ifpim123g  42183  ifpor123g  42191  rp-fakeoranass  42197  ontric3g  42205  frege133d  42448  or3or  42706  undif3VD  43575  wallispilem3  44717  iccpartgt  46029  nnsum4primeseven  46402  nnsum4primesevenALTV  46403  lindslinindsimp2  47045