Theorem orbi2i 913

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

Syntax hints:   ↔ wb 209   ∨ 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 210  df-or 848

This theorem is referenced by:  orbi1i  914  orbi12i  915  orass  922  or4  927  or42  928  orordir  930  dn1  1058  dfifp6  1069  excxor  1513  nf3  1794  nfnbiOLD  1863  19.44v  2002  19.44  2237  sspsstri  4003  unass  4066  undi  4175  undif3  4191  2nreu  4342  undif4  4367  ssunpr  4731  sspr  4732  sstp  4733  pr1eqbg  4753  iinun2  4967  iinuni  4992  qfto  5966  somin1  5978  ordtri2  6226  on0eqel  6309  frxp  7871  frrlem12  8016  wfrlem14  8046  wfrlem15  8047  supgtoreq  9064  wemapsolem  9144  fin1a2lem12  9990  psslinpr  10610  suplem2pr  10632  fimaxre  11741  elnn0  12057  elxnn0  12129  elnn1uz2  12486  elxr  12673  xrinfmss  12865  elfzp1  13127  hashf1lem2  13987  dvdslelem  15833  pythagtrip  16350  tosso  17879  maducoeval2  21491  madugsum  21494  ist0-3  22196  limcdif  24727  ellimc2  24728  limcmpt  24734  limcres  24737  plydivex  25144  taylfval  25205  legtrid  26636  legso  26644  lmicom  26833  numedglnl  27189  nb3grprlem2  27423  clwwlkneq0  28066  atomli  30417  atoml2i  30418  or3di  30483  disjnf  30582  disjex  30604  disjexc  30605  cycpmrn  31083  orngsqr  31176  ind1a  31653  esumcvg  31720  voliune  31863  volfiniune  31864  bnj964  32590  satfvsucsuc  32994  satfrnmapom  32999  satf0op  33006  fmlaomn0  33019  dfso2  33391  poxp2  33470  poxp3  33476  soseq  33483  lineunray  34135  bj-dfbi4  34440  wl-ifpimpr  35323  wl-df4-3mintru2  35344  poimirlem18  35481  poimirlem23  35486  poimirlem27  35490  poimirlem31  35494  itg2addnclem2  35515  tsxo1  35981  tsxo2  35982  tsxo3  35983  tsxo4  35984  tsna1  35988  tsna2  35989  tsna3  35990  ts3an1  35994  ts3an2  35995  ts3an3  35996  ts3or1  35997  ts3or2  35998  ts3or3  35999  dfeldisj5  36518  ifpim123g  40733  ifpor123g  40741  rp-fakeoranass  40747  ontric3g  40755  frege133d  40991  or3or  41249  undif3VD  42116  wallispilem3  43226  iccpartgt  44495  nnsum4primeseven  44868  nnsum4primesevenALTV  44869  lindslinindsimp2  45420