Theorem orbi2i 926

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

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  orbi1i  927  orbi12i  928  orass  935  or4  940  or42  941  orordir  943  dn1  1073  dfifp6  1084  excxor  1546  nf3  1819  19.44v  2031  19.44  2274  sspsstri  4054  unass  4118  undi  4231  undif3  4246  2nreu  4402  undif4  4420  ssunpr  4794  sspr  4795  sstp  4796  pr1eqbg  4817  iinun2  5031  iinuni  5058  qfto  6115  somin1  6127  ordtri2  6397  on0eqel  6487  frxp  8136  poxp2  8153  soseq  8169  frrlem12  8308  supgtoreq  9456  wemapsolem  9537  fin1a2lem12  10482  psslinpr  11109  suplem2pr  11131  fimaxre  12254  ind1a  12324  elnn0  12601  elxnn0  12674  elnn1uz2  13045  elxr  13238  xrinfmss  13433  elfzp1  13701  hashf1lem2  14594  dvdslelem  16472  pythagtrip  17005  tosso  18584  orngsqr  21116  maducoeval2  22948  madugsum  22951  ist0-3  23656  limcdif  26189  ellimc2  26190  limcmpt  26196  limcres  26199  plydivex  26611  taylfval  26679  precsexlem9  28594  z12zsodd  28861  legtrid  29047  legso  29055  lmicom  29286  numedglnl  29715  nb3grprlem2  29955  clwwlkneq0  30613  atomli  32977  atoml2i  32978  or3di  33050  disjnf  33157  disjex  33179  disjexc  33180  cycpmrn  33697  esumcvg  34711  voliune  34855  volfiniune  34856  bnj964  35566  satfvsucsuc  36109  satfrnmapom  36114  satf0op  36121  fmlaomn0  36134  dfso2  36499  lineunray  36892  bj-dfbi4  37423  bj-axadj  37934  wl-ifpimpr  38369  wl-df4-3mintru2  38390  poimirlem18  38536  poimirlem23  38541  poimirlem27  38545  poimirlem31  38549  itg2addnclem2  38570  tsxo1  39049  tsxo2  39050  tsxo3  39051  tsxo4  39052  tsna1  39056  tsna2  39057  tsna3  39058  ts3an1  39062  ts3an2  39063  ts3an3  39064  ts3or1  39065  ts3or2  39066  ts3or3  39067  dfeldisj5  39725  aks4d1p7  43113  reelznn0nn  43505  dflim5  44315  ifpim123g  44485  ifpor123g  44493  rp-fakeoranass  44499  ontric3g  44507  frege133d  44750  or3or  45008  undif3VD  45849  wallispilem3  47046  iccpartgt  48478  nnsum4primeseven  48867  nnsum4primesevenALTV  48868  clnbupgrel  48901  usgrexmpl2trifr  49104  pg4cyclnex  49194  lindslinindsimp2  49544  veronesevrowd  50948