Theorem orbi2i 913

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

Syntax hints:   ↔ wb 206   ∨ wo 848

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 849

This theorem is referenced by:  orbi1i  914  orbi12i  915  orass  922  or4  927  or42  928  orordir  930  dn1  1058  dfifp6  1069  excxor  1518  nf3  1788  19.44v  2000  19.44  2245  sspsstri  4046  unass  4113  undi  4226  undif3  4241  2nreu  4385  undif4  4408  ssunpr  4778  sspr  4779  sstp  4780  pr1eqbg  4801  iinun2  5016  iinuni  5041  qfto  6079  somin1  6091  ordtri2  6353  on0eqel  6443  frxp  8070  poxp2  8087  soseq  8103  frrlem12  8241  supgtoreq  9378  wemapsolem  9459  fin1a2lem12  10327  psslinpr  10948  suplem2pr  10970  fimaxre  12094  ind1a  12164  elnn0  12433  elxnn0  12506  elnn1uz2  12869  elxr  13061  xrinfmss  13256  elfzp1  13522  hashf1lem2  14412  dvdslelem  16272  pythagtrip  16799  tosso  18377  orngsqr  20837  maducoeval2  22618  madugsum  22621  ist0-3  23323  limcdif  25856  ellimc2  25857  limcmpt  25863  limcres  25866  plydivex  26277  taylfval  26338  precsexlem9  28224  z12zsodd  28491  legtrid  28676  legso  28684  lmicom  28873  numedglnl  29230  nb3grprlem2  29467  clwwlkneq0  30117  atomli  32471  atoml2i  32472  or3di  32546  disjnf  32658  disjex  32680  disjexc  32681  cycpmrn  33222  esumcvg  34249  voliune  34392  volfiniune  34393  bnj964  35104  satfvsucsuc  35566  satfrnmapom  35571  satf0op  35578  fmlaomn0  35591  dfso2  35956  lineunray  36348  bj-dfbi4  36857  bj-axadj  37367  wl-ifpimpr  37799  wl-df4-3mintru2  37820  poimirlem18  37976  poimirlem23  37981  poimirlem27  37985  poimirlem31  37989  itg2addnclem2  38010  tsxo1  38475  tsxo2  38476  tsxo3  38477  tsxo4  38478  tsna1  38482  tsna2  38483  tsna3  38484  ts3an1  38488  ts3an2  38489  ts3an3  38490  ts3or1  38491  ts3or2  38492  ts3or3  38493  dfeldisj5  39151  aks4d1p7  42539  reelznn0nn  42923  dflim5  43778  ifpim123g  43948  ifpor123g  43956  rp-fakeoranass  43962  ontric3g  43970  frege133d  44213  or3or  44471  undif3VD  45329  wallispilem3  46516  iccpartgt  47902  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  clnbupgrel  48325  usgrexmpl2trifr  48528  pg4cyclnex  48618  lindslinindsimp2  48954