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  1545  nf3  1818  19.44v  2030  19.44  2273  sspsstri  4032  unass  4169  undi  4229  undif3  4244  2nreu  4401  undif4  4419  ssunpr  4788  sspr  4789  sstp  4790  pr1eqbg  4811  iinun2  5030  iinuni  5057  qfto  6117  somin1  6129  ordtri2  6401  on0eqel  6491  frxp  8144  poxp2  8166  soseq  8182  frrlem12  8322  supgtoreq  9470  wemapsolem  9551  fin1a2lem12  10496  psslinpr  11123  suplem2pr  11145  fimaxre  12268  ind1a  12338  elnn0  12615  elxnn0  12688  elnn1uz2  13059  elxr  13252  xrinfmss  13447  elfzp1  13715  hashf1lem2  14608  dvdslelem  16488  pythagtrip  17021  tosso  18600  orngsqr  21132  maducoeval2  22964  madugsum  22967  ist0-3  23672  limcdif  26205  ellimc2  26206  limcmpt  26212  limcres  26215  plydivex  26627  taylfval  26695  precsexlem9  28610  z12zsodd  28877  legtrid  29063  legso  29071  lmicom  29302  numedglnl  29731  nb3grprlem2  29971  clwwlkneq0  30629  atomli  32993  atoml2i  32994  or3di  33108  disjnf  33215  disjex  33237  disjexc  33238  cycpmrn  33754  esumcvg  34768  voliune  34912  volfiniune  34913  bnj964  35623  satfvsucsuc  36220  satfrnmapom  36225  satf0op  36232  fmlaomn0  36245  dfso2  36616  lineunray  37008  bj-dfbi4  37539  bj-axadj  38050  wl-ifpimpr  38498  wl-df4-3mintru2  38519  poimirlem18  38665  poimirlem23  38670  poimirlem27  38674  poimirlem31  38678  itg2addnclem2  38699  tsxo1  39178  tsxo2  39179  tsxo3  39180  tsxo4  39181  tsna1  39185  tsna2  39186  tsna3  39187  ts3an1  39191  ts3an2  39192  ts3an3  39193  ts3or1  39194  ts3or2  39195  ts3or3  39196  dfeldisj5  39854  aks4d1p7  43242  reelznn0nn  43634  dflim5  44440  ifpim123g  44610  ifpor123g  44618  rp-fakeoranass  44624  ontric3g  44632  frege133d  44874  or3or  45132  undif3VD  45972  wallispilem3  47185  iccpartgt  48617  nnsum4primeseven  49006  nnsum4primesevenALTV  49007  clnbupgrel  49040  usgrexmpl2trifr  49243  pg4cyclnex  49333  lindslinindsimp2  49683  veronesevrowd  51162