Theorem orbi2i 909

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

Syntax hints:   ↔ wb 208   ∨ wo 843

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 209  df-or 844

This theorem is referenced by:  orbi1i  910  orbi12i  911  orass  918  or4  923  or42  924  orordir  926  dn1  1052  dfifp6  1063  excxor  1507  nf3  1787  nfnbi  1855  19.44v  1999  19.44  2239  r19.30OLD  3341  sspsstri  4081  unass  4144  undi  4253  undif3  4267  2nreu  4395  undif4  4418  ssunpr  4767  sspr  4768  sstp  4769  pr1eqbg  4789  iinun2  4997  iinuni  5022  qfto  5983  somin1  5995  ordtri2  6228  on0eqel  6310  frxp  7822  wfrlem14  7970  wfrlem15  7971  supgtoreq  8936  wemapsolem  9016  fin1a2lem12  9835  psslinpr  10455  suplem2pr  10477  fimaxre  11586  fimaxreOLD  11587  elnn0  11902  elxnn0  11972  elnn1uz2  12328  elxr  12514  xrinfmss  12706  elfzp1  12960  hashf1lem2  13817  dvdslelem  15661  pythagtrip  16173  tosso  17648  maducoeval2  21251  madugsum  21254  ist0-3  21955  limcdif  24476  ellimc2  24477  limcmpt  24483  limcres  24486  plydivex  24888  taylfval  24949  legtrid  26379  legso  26387  lmicom  26576  numedglnl  26931  nb3grprlem2  27165  clwwlkneq0  27809  atomli  30161  atoml2i  30162  or3di  30227  disjnf  30322  disjex  30344  disjexc  30345  cycpmrn  30787  orngsqr  30879  ind1a  31280  esumcvg  31347  voliune  31490  volfiniune  31491  bnj964  32217  satfvsucsuc  32614  satfrnmapom  32619  satf0op  32626  fmlaomn0  32639  dfso2  32992  soseq  33098  frrlem12  33136  lineunray  33610  bj-dfbi4  33908  poimirlem18  34912  poimirlem23  34917  poimirlem27  34921  poimirlem31  34925  itg2addnclem2  34946  tsxo1  35417  tsxo2  35418  tsxo3  35419  tsxo4  35420  tsna1  35424  tsna2  35425  tsna3  35426  ts3an1  35430  ts3an2  35431  ts3an3  35432  ts3or1  35433  ts3or2  35434  ts3or3  35435  dfeldisj5  35956  ifpim123g  39873  ifpor123g  39881  rp-fakeoranass  39887  ontric3g  39895  frege133d  40117  or3or  40378  undif3VD  41223  wallispilem3  42359  iccpartgt  43594  nnsum4primeseven  43972  nnsum4primesevenALTV  43973  lindslinindsimp2  44525