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  2240  sspsstri  4052  unass  4119  undi  4232  undif3  4247  2nreu  4391  undif4  4414  ssunpr  4783  sspr  4784  sstp  4785  pr1eqbg  4806  iinun2  5019  iinuni  5044  qfto  6067  somin1  6079  ordtri2  6341  on0eqel  6431  frxp  8056  poxp2  8073  soseq  8089  frrlem12  8227  supgtoreq  9355  wemapsolem  9436  fin1a2lem12  10302  psslinpr  10922  suplem2pr  10944  fimaxre  12066  elnn0  12383  elxnn0  12456  elnn1uz2  12823  elxr  13015  xrinfmss  13209  elfzp1  13474  hashf1lem2  14363  dvdslelem  16220  pythagtrip  16746  tosso  18323  orngsqr  20781  maducoeval2  22555  madugsum  22558  ist0-3  23260  limcdif  25804  ellimc2  25805  limcmpt  25811  limcres  25814  plydivex  26232  taylfval  26293  precsexlem9  28153  zs12zodd  28392  legtrid  28569  legso  28577  lmicom  28766  numedglnl  29122  nb3grprlem2  29359  clwwlkneq0  30009  atomli  32362  atoml2i  32363  or3di  32438  disjnf  32550  disjex  32572  disjexc  32573  ind1a  32840  cycpmrn  33112  esumcvg  34099  voliune  34242  volfiniune  34243  bnj964  34955  satfvsucsuc  35409  satfrnmapom  35414  satf0op  35421  fmlaomn0  35434  dfso2  35799  lineunray  36189  bj-dfbi4  36615  bj-axadj  37083  wl-ifpimpr  37508  wl-df4-3mintru2  37529  poimirlem18  37686  poimirlem23  37691  poimirlem27  37695  poimirlem31  37699  itg2addnclem2  37720  tsxo1  38185  tsxo2  38186  tsxo3  38187  tsxo4  38188  tsna1  38192  tsna2  38193  tsna3  38194  ts3an1  38198  ts3an2  38199  ts3an3  38200  ts3or1  38201  ts3or2  38202  ts3or3  38203  dfeldisj5  38767  aks4d1p7  42124  reelznn0nn  42502  dflim5  43370  ifpim123g  43541  ifpor123g  43549  rp-fakeoranass  43555  ontric3g  43563  frege133d  43806  or3or  44064  undif3VD  44922  wallispilem3  46113  iccpartgt  47466  nnsum4primeseven  47839  nnsum4primesevenALTV  47840  clnbupgrel  47873  usgrexmpl2trifr  48076  pg4cyclnex  48166  lindslinindsimp2  48503