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  1516  nf3  1786  19.44v  1998  19.44  2238  sspsstri  4056  unass  4123  undi  4236  undif3  4251  2nreu  4395  undif4  4418  ssunpr  4785  sspr  4786  sstp  4787  pr1eqbg  4808  iinun2  5022  iinuni  5047  qfto  6070  somin1  6082  ordtri2  6342  on0eqel  6432  frxp  8059  poxp2  8076  soseq  8092  frrlem12  8230  supgtoreq  9361  wemapsolem  9442  fin1a2lem12  10305  psslinpr  10925  suplem2pr  10947  fimaxre  12069  elnn0  12386  elxnn0  12459  elnn1uz2  12826  elxr  13018  xrinfmss  13212  elfzp1  13477  hashf1lem2  14363  dvdslelem  16220  pythagtrip  16746  tosso  18323  orngsqr  20751  maducoeval2  22525  madugsum  22528  ist0-3  23230  limcdif  25775  ellimc2  25776  limcmpt  25782  limcres  25785  plydivex  26203  taylfval  26264  precsexlem9  28122  zs12zodd  28359  legtrid  28536  legso  28544  lmicom  28733  numedglnl  29089  nb3grprlem2  29326  clwwlkneq0  29973  atomli  32326  atoml2i  32327  or3di  32403  disjnf  32514  disjex  32536  disjexc  32537  ind1a  32802  cycpmrn  33085  esumcvg  34053  voliune  34196  volfiniune  34197  bnj964  34910  satfvsucsuc  35338  satfrnmapom  35343  satf0op  35350  fmlaomn0  35363  dfso2  35728  lineunray  36121  bj-dfbi4  36547  bj-axadj  37015  wl-ifpimpr  37440  wl-df4-3mintru2  37461  poimirlem18  37618  poimirlem23  37623  poimirlem27  37627  poimirlem31  37631  itg2addnclem2  37652  tsxo1  38117  tsxo2  38118  tsxo3  38119  tsxo4  38120  tsna1  38124  tsna2  38125  tsna3  38126  ts3an1  38130  ts3an2  38131  ts3an3  38132  ts3or1  38133  ts3or2  38134  ts3or3  38135  dfeldisj5  38699  aks4d1p7  42056  reelznn0nn  42434  dflim5  43302  ifpim123g  43473  ifpor123g  43481  rp-fakeoranass  43487  ontric3g  43495  frege133d  43738  or3or  43996  undif3VD  44855  wallispilem3  46048  iccpartgt  47411  nnsum4primeseven  47784  nnsum4primesevenALTV  47785  clnbupgrel  47818  usgrexmpl2trifr  48021  pg4cyclnex  48111  lindslinindsimp2  48448