Theorem orbi2i 925

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

Syntax hints:   ↔ wb 209   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  orbi1i  926  orbi12i  927  orass  934  or4  939  or42  940  orordir  942  dn1  1073  dfifp6  1084  excxor  1546  nf3  1816  19.44v  2028  19.44  2273  sspsstri  4060  unass  4125  undi  4238  undif3  4253  2nreu  4409  undif4  4427  ssunpr  4799  sspr  4800  sstp  4801  pr1eqbg  4822  iinun2  5037  iinuni  5064  qfto  6121  somin1  6133  ordtri2  6396  on0eqel  6486  frxp  8118  poxp2  8135  soseq  8151  frrlem12  8290  supgtoreq  9427  wemapsolem  9508  fin1a2lem12  10390  psslinpr  11011  suplem2pr  11033  fimaxre  12154  ind1a  12224  elnn0  12501  elxnn0  12574  elnn1uz2  12944  elxr  13136  xrinfmss  13331  elfzp1  13598  hashf1lem2  14489  dvdslelem  16362  pythagtrip  16889  tosso  18468  orngsqr  20969  maducoeval2  22797  madugsum  22800  ist0-3  23502  limcdif  26035  ellimc2  26036  limcmpt  26042  limcres  26045  plydivex  26458  taylfval  26522  precsexlem9  28408  z12zsodd  28675  legtrid  28860  legso  28868  lmicom  29097  numedglnl  29494  nb3grprlem2  29731  clwwlkneq0  30380  atomli  32734  atoml2i  32735  or3di  32807  disjnf  32915  disjex  32937  disjexc  32938  cycpmrn  33463  esumcvg  34476  voliune  34619  volfiniune  34620  bnj964  35331  satfvsucsuc  35857  satfrnmapom  35862  satf0op  35869  fmlaomn0  35882  dfso2  36247  lineunray  36639  bj-dfbi4  37166  bj-axadj  37677  wl-ifpimpr  38112  wl-df4-3mintru2  38133  poimirlem18  38289  poimirlem23  38294  poimirlem27  38298  poimirlem31  38302  itg2addnclem2  38323  tsxo1  38786  tsxo2  38787  tsxo3  38788  tsxo4  38789  tsna1  38793  tsna2  38794  tsna3  38795  ts3an1  38799  ts3an2  38800  ts3an3  38801  ts3or1  38802  ts3or2  38803  ts3or3  38804  dfeldisj5  39462  aks4d1p7  42850  reelznn0nn  43235  dflim5  44056  ifpim123g  44226  ifpor123g  44234  rp-fakeoranass  44240  ontric3g  44248  frege133d  44491  or3or  44749  undif3VD  45590  wallispilem3  46781  iccpartgt  48176  nnsum4primeseven  48565  nnsum4primesevenALTV  48566  clnbupgrel  48599  usgrexmpl2trifr  48802  pg4cyclnex  48892  lindslinindsimp2  49243