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

Syntax hints:   ↔ wb 206   ∨ wo 847

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 848

This theorem is referenced by:  orbi1i  913  orbi12i  914  orass  921  or4  926  or42  927  orordir  929  dn1  1057  dfifp6  1068  excxor  1516  nf3  1786  19.44v  1998  19.44  2238  sspsstri  4064  unass  4131  undi  4244  undif3  4259  2nreu  4403  undif4  4426  ssunpr  4794  sspr  4795  sstp  4796  pr1eqbg  4817  iinun2  5032  iinuni  5057  qfto  6082  somin1  6094  ordtri2  6355  on0eqel  6446  frxp  8082  poxp2  8099  soseq  8115  frrlem12  8253  supgtoreq  9398  wemapsolem  9479  fin1a2lem12  10340  psslinpr  10960  suplem2pr  10982  fimaxre  12103  elnn0  12420  elxnn0  12493  elnn1uz2  12860  elxr  13052  xrinfmss  13246  elfzp1  13511  hashf1lem2  14397  dvdslelem  16255  pythagtrip  16781  tosso  18354  maducoeval2  22503  madugsum  22506  ist0-3  23208  limcdif  25753  ellimc2  25754  limcmpt  25760  limcres  25763  plydivex  26181  taylfval  26242  precsexlem9  28093  legtrid  28494  legso  28502  lmicom  28691  numedglnl  29047  nb3grprlem2  29284  clwwlkneq0  29931  atomli  32284  atoml2i  32285  or3di  32361  disjnf  32472  disjex  32494  disjexc  32495  ind1a  32755  cycpmrn  33073  orngsqr  33255  esumcvg  34049  voliune  34192  volfiniune  34193  bnj964  34906  satfvsucsuc  35325  satfrnmapom  35330  satf0op  35337  fmlaomn0  35350  dfso2  35715  lineunray  36108  bj-dfbi4  36534  bj-axadj  37002  wl-ifpimpr  37427  wl-df4-3mintru2  37448  poimirlem18  37605  poimirlem23  37610  poimirlem27  37614  poimirlem31  37618  itg2addnclem2  37639  tsxo1  38104  tsxo2  38105  tsxo3  38106  tsxo4  38107  tsna1  38111  tsna2  38112  tsna3  38113  ts3an1  38117  ts3an2  38118  ts3an3  38119  ts3or1  38120  ts3or2  38121  ts3or3  38122  dfeldisj5  38686  aks4d1p7  42044  reelznn0nn  42422  dflim5  43291  ifpim123g  43462  ifpor123g  43470  rp-fakeoranass  43476  ontric3g  43484  frege133d  43727  or3or  43985  undif3VD  44844  wallispilem3  46038  iccpartgt  47401  nnsum4primeseven  47774  nnsum4primesevenALTV  47775  clnbupgrel  47808  usgrexmpl2trifr  48001  pg4cyclnex  48090  lindslinindsimp2  48425