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  1992  19.44  2237  sspsstri  4080  unass  4147  undi  4260  undif3  4275  2nreu  4419  undif4  4442  ssunpr  4810  sspr  4811  sstp  4812  pr1eqbg  4833  iinun2  5049  iinuni  5074  qfto  6110  somin1  6122  ordtri2  6387  on0eqel  6477  frxp  8123  poxp2  8140  soseq  8156  frrlem12  8294  wfrlem14OLD  8334  wfrlem15OLD  8335  supgtoreq  9481  wemapsolem  9562  fin1a2lem12  10423  psslinpr  11043  suplem2pr  11065  fimaxre  12184  elnn0  12501  elxnn0  12574  elnn1uz2  12939  elxr  13130  xrinfmss  13324  elfzp1  13589  hashf1lem2  14472  dvdslelem  16326  pythagtrip  16852  tosso  18427  maducoeval2  22576  madugsum  22579  ist0-3  23281  limcdif  25827  ellimc2  25828  limcmpt  25834  limcres  25837  plydivex  26255  taylfval  26316  precsexlem9  28156  legtrid  28516  legso  28524  lmicom  28713  numedglnl  29069  nb3grprlem2  29306  clwwlkneq0  29956  atomli  32309  atoml2i  32310  or3di  32386  disjnf  32497  disjex  32519  disjexc  32520  ind1a  32782  cycpmrn  33100  orngsqr  33272  esumcvg  34063  voliune  34206  volfiniune  34207  bnj964  34920  satfvsucsuc  35333  satfrnmapom  35338  satf0op  35345  fmlaomn0  35358  dfso2  35718  lineunray  36111  bj-dfbi4  36537  bj-axadj  37005  wl-ifpimpr  37430  wl-df4-3mintru2  37451  poimirlem18  37608  poimirlem23  37613  poimirlem27  37617  poimirlem31  37621  itg2addnclem2  37642  tsxo1  38107  tsxo2  38108  tsxo3  38109  tsxo4  38110  tsna1  38114  tsna2  38115  tsna3  38116  ts3an1  38120  ts3an2  38121  ts3an3  38122  ts3or1  38123  ts3or2  38124  ts3or3  38125  dfeldisj5  38685  aks4d1p7  42042  reelznn0nn  42439  dflim5  43300  ifpim123g  43471  ifpor123g  43479  rp-fakeoranass  43485  ontric3g  43493  frege133d  43736  or3or  43994  undif3VD  44854  wallispilem3  46044  iccpartgt  47389  nnsum4primeseven  47762  nnsum4primesevenALTV  47763  clnbupgrel  47796  usgrexmpl2trifr  47989  lindslinindsimp2  48387