Theorem orbi2i 912

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

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

This theorem is referenced by:  orbi1i  913  orbi12i  914  orass  921  or4  926  or42  927  orordir  929  dn1  1057  dfifp6  1068  excxor  1517  nf3  1787  19.44v  1999  19.44  2244  sspsstri  4057  unass  4124  undi  4237  undif3  4252  2nreu  4396  undif4  4419  ssunpr  4790  sspr  4791  sstp  4792  pr1eqbg  4813  iinun2  5028  iinuni  5053  qfto  6078  somin1  6090  ordtri2  6352  on0eqel  6442  frxp  8068  poxp2  8085  soseq  8101  frrlem12  8239  supgtoreq  9374  wemapsolem  9455  fin1a2lem12  10321  psslinpr  10942  suplem2pr  10964  fimaxre  12086  elnn0  12403  elxnn0  12476  elnn1uz2  12838  elxr  13030  xrinfmss  13225  elfzp1  13490  hashf1lem2  14379  dvdslelem  16236  pythagtrip  16762  tosso  18340  orngsqr  20799  maducoeval2  22584  madugsum  22587  ist0-3  23289  limcdif  25833  ellimc2  25834  limcmpt  25840  limcres  25843  plydivex  26261  taylfval  26322  precsexlem9  28211  z12zsodd  28478  legtrid  28663  legso  28671  lmicom  28860  numedglnl  29217  nb3grprlem2  29454  clwwlkneq0  30104  atomli  32457  atoml2i  32458  or3di  32533  disjnf  32645  disjex  32667  disjexc  32668  ind1a  32938  cycpmrn  33225  esumcvg  34243  voliune  34386  volfiniune  34387  bnj964  35099  satfvsucsuc  35559  satfrnmapom  35564  satf0op  35571  fmlaomn0  35584  dfso2  35949  lineunray  36341  bj-dfbi4  36773  bj-axadj  37242  wl-ifpimpr  37671  wl-df4-3mintru2  37692  poimirlem18  37839  poimirlem23  37844  poimirlem27  37848  poimirlem31  37852  itg2addnclem2  37873  tsxo1  38338  tsxo2  38339  tsxo3  38340  tsxo4  38341  tsna1  38345  tsna2  38346  tsna3  38347  ts3an1  38351  ts3an2  38352  ts3an3  38353  ts3or1  38354  ts3or2  38355  ts3or3  38356  dfeldisj5  38980  aks4d1p7  42337  reelznn0nn  42716  dflim5  43571  ifpim123g  43741  ifpor123g  43749  rp-fakeoranass  43755  ontric3g  43763  frege133d  44006  or3or  44264  undif3VD  45122  wallispilem3  46311  iccpartgt  47673  nnsum4primeseven  48046  nnsum4primesevenALTV  48047  clnbupgrel  48080  usgrexmpl2trifr  48283  pg4cyclnex  48373  lindslinindsimp2  48709