Theorem orbi2i 913

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

Syntax hints:   ↔ wb 206   ∨ wo 848

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 849

This theorem is referenced by:  orbi1i  914  orbi12i  915  orass  922  or4  927  or42  928  orordir  930  dn1  1058  dfifp6  1069  excxor  1518  nf3  1788  19.44v  2000  19.44  2245  sspsstri  4059  unass  4126  undi  4239  undif3  4254  2nreu  4398  undif4  4421  ssunpr  4792  sspr  4793  sstp  4794  pr1eqbg  4815  iinun2  5030  iinuni  5055  qfto  6086  somin1  6098  ordtri2  6360  on0eqel  6450  frxp  8078  poxp2  8095  soseq  8111  frrlem12  8249  supgtoreq  9386  wemapsolem  9467  fin1a2lem12  10333  psslinpr  10954  suplem2pr  10976  fimaxre  12098  elnn0  12415  elxnn0  12488  elnn1uz2  12850  elxr  13042  xrinfmss  13237  elfzp1  13502  hashf1lem2  14391  dvdslelem  16248  pythagtrip  16774  tosso  18352  orngsqr  20811  maducoeval2  22596  madugsum  22599  ist0-3  23301  limcdif  25845  ellimc2  25846  limcmpt  25852  limcres  25855  plydivex  26273  taylfval  26334  precsexlem9  28223  z12zsodd  28490  legtrid  28675  legso  28683  lmicom  28872  numedglnl  29229  nb3grprlem2  29466  clwwlkneq0  30116  atomli  32470  atoml2i  32471  or3di  32545  disjnf  32657  disjex  32679  disjexc  32680  ind1a  32949  cycpmrn  33237  esumcvg  34264  voliune  34407  volfiniune  34408  bnj964  35119  satfvsucsuc  35581  satfrnmapom  35586  satf0op  35593  fmlaomn0  35606  dfso2  35971  lineunray  36363  bj-dfbi4  36798  bj-axadj  37289  wl-ifpimpr  37721  wl-df4-3mintru2  37742  poimirlem18  37889  poimirlem23  37894  poimirlem27  37898  poimirlem31  37902  itg2addnclem2  37923  tsxo1  38388  tsxo2  38389  tsxo3  38390  tsxo4  38391  tsna1  38395  tsna2  38396  tsna3  38397  ts3an1  38401  ts3an2  38402  ts3an3  38403  ts3or1  38404  ts3or2  38405  ts3or3  38406  dfeldisj5  39064  aks4d1p7  42453  reelznn0nn  42831  dflim5  43686  ifpim123g  43856  ifpor123g  43864  rp-fakeoranass  43870  ontric3g  43878  frege133d  44121  or3or  44379  undif3VD  45237  wallispilem3  46425  iccpartgt  47787  nnsum4primeseven  48160  nnsum4primesevenALTV  48161  clnbupgrel  48194  usgrexmpl2trifr  48397  pg4cyclnex  48487  lindslinindsimp2  48823