Theorem orbi2i 886

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

Syntax hints:   ↔ wb 196   ∨ wo 826

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 197  df-or 827

This theorem is referenced by:  orbi1i  887  orbi12i  888  orass  895  or4  900  or42  901  orordir  903  dn1  1045  dfifp6  1055  3orcombOLD  1079  excxor  1617  nf3  1860  nfnbi  1931  19.44v  2080  19.44  2262  r19.30  3230  sspsstri  3859  unass  3921  undi  4023  undif3  4037  undif4  4177  ssunpr  4498  sspr  4499  sstp  4500  pr1eqbg  4521  iinun2  4720  iinuni  4743  qfto  5658  somin1  5670  ordtri2  5901  on0eqel  5988  frxp  7438  wfrlem14  7581  wfrlem15  7582  supgtoreq  8532  wemapsolem  8611  fin1a2lem12  9435  psslinpr  10055  suplem2pr  10077  fimaxre  11170  elnn0  11496  elxnn0  11567  elnn1uz2  11968  elxr  12155  xrinfmss  12345  elfzp1  12598  hashf1lem2  13442  dvdslelem  15240  pythagtrip  15746  tosso  17244  maducoeval2  20664  madugsum  20667  ist0-3  21370  limcdif  23860  ellimc2  23861  limcmpt  23867  limcres  23870  plydivex  24272  taylfval  24333  legtrid  25707  legso  25715  lmicom  25901  numedglnl  26261  nb3grprlem2  26506  clwwlkneq0  27183  numclwwlk3lemOLD  27580  atomli  29581  atoml2i  29582  or3di  29647  disjnf  29722  disjex  29743  disjexc  29744  orngsqr  30144  ind1a  30421  esumcvg  30488  voliune  30632  volfiniune  30633  bnj964  31351  dfso2  31982  soseq  32091  lineunray  32591  bj-dfbi4  32895  poimirlem18  33760  poimirlem23  33765  poimirlem27  33769  poimirlem31  33773  itg2addnclem2  33794  tsxo1  34276  tsxo2  34277  tsxo3  34278  tsxo4  34279  tsna1  34283  tsna2  34284  tsna3  34285  ts3an1  34289  ts3an2  34290  ts3an3  34291  ts3or1  34292  ts3or2  34293  ts3or3  34294  ifpim123g  38371  ifpor123g  38379  rp-fakeoranass  38385  frege133d  38583  or3or  38845  undif3VD  39640  wallispilem3  40801  iccpartgt  41891  nnsum4primeseven  42216  nnsum4primesevenALTV  42217  lindslinindsimp2  42780