Theorem orbi2i 896

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

Syntax hints:   ↔ wb 198   ∨ wo 833

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 199  df-or 834

This theorem is referenced by:  orbi1i  897  orbi12i  898  orass  905  or4  910  or42  911  orordir  913  dn1  1038  dfifp6  1049  excxor  1493  nf3  1749  nfnbi  1817  19.44v  1949  19.44  2170  r19.30OLD  3280  sspsstri  3969  unass  4031  undi  4138  undif3  4152  2nreu  4276  undif4  4299  ssunpr  4639  sspr  4640  sstp  4641  pr1eqbg  4661  iinun2  4861  iinuni  4886  qfto  5821  somin1  5833  ordtri2  6064  on0eqel  6146  frxp  7625  wfrlem14  7772  wfrlem15  7773  supgtoreq  8729  wemapsolem  8809  fin1a2lem12  9631  psslinpr  10251  suplem2pr  10273  fimaxre  11385  fimaxreOLD  11386  elnn0  11709  elxnn0  11781  elnn1uz2  12139  elxr  12328  xrinfmss  12519  elfzp1  12773  hashf1lem2  13627  dvdslelem  15519  pythagtrip  16027  tosso  17504  maducoeval2  20953  madugsum  20956  ist0-3  21657  limcdif  24177  ellimc2  24178  limcmpt  24184  limcres  24187  plydivex  24589  taylfval  24650  legtrid  26079  legso  26087  lmicom  26276  numedglnl  26632  nb3grprlem2  26866  clwwlkneq0  27544  atomli  29940  atoml2i  29941  or3di  30006  disjnf  30087  disjex  30108  disjexc  30109  orngsqr  30562  ind1a  30928  esumcvg  30995  voliune  31139  volfiniune  31140  bnj964  31868  satf0op  32193  dfso2  32516  soseq  32623  frrlem12  32661  lineunray  33135  bj-dfbi4  33429  poimirlem18  34357  poimirlem23  34362  poimirlem27  34366  poimirlem31  34370  itg2addnclem2  34391  tsxo1  34865  tsxo2  34866  tsxo3  34867  tsxo4  34868  tsna1  34872  tsna2  34873  tsna3  34874  ts3an1  34878  ts3an2  34879  ts3an3  34880  ts3or1  34881  ts3or2  34882  ts3or3  34883  dfeldisj5  35405  ifpim123g  39268  ifpor123g  39276  rp-fakeoranass  39282  frege133d  39479  or3or  39740  undif3VD  40641  wallispilem3  41789  iccpartgt  42965  nnsum4primeseven  43339  nnsum4primesevenALTV  43340  lindslinindsimp2  43891