Theorem orbi2i 909

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

Syntax hints:   ↔ wb 208   ∨ wo 843

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 209  df-or 844

This theorem is referenced by:  orbi1i  910  orbi12i  911  orass  918  or4  923  or42  924  orordir  926  dn1  1052  dfifp6  1063  excxor  1507  nf3  1786  nfnbi  1854  19.44v  1998  19.44  2238  r19.30OLD  3342  sspsstri  4082  unass  4145  undi  4254  undif3  4268  2nreu  4396  undif4  4419  ssunpr  4768  sspr  4769  sstp  4770  pr1eqbg  4790  iinun2  4998  iinuni  5023  qfto  5984  somin1  5996  ordtri2  6229  on0eqel  6311  frxp  7823  wfrlem14  7971  wfrlem15  7972  supgtoreq  8937  wemapsolem  9017  fin1a2lem12  9836  psslinpr  10456  suplem2pr  10478  fimaxre  11587  fimaxreOLD  11588  elnn0  11902  elxnn0  11972  elnn1uz2  12328  elxr  12514  xrinfmss  12706  elfzp1  12960  hashf1lem2  13817  dvdslelem  15662  pythagtrip  16174  tosso  17649  maducoeval2  21252  madugsum  21255  ist0-3  21956  limcdif  24477  ellimc2  24478  limcmpt  24484  limcres  24487  plydivex  24889  taylfval  24950  legtrid  26380  legso  26388  lmicom  26577  numedglnl  26932  nb3grprlem2  27166  clwwlkneq0  27810  atomli  30162  atoml2i  30163  or3di  30228  disjnf  30323  disjex  30345  disjexc  30346  cycpmrn  30789  orngsqr  30881  ind1a  31282  esumcvg  31349  voliune  31492  volfiniune  31493  bnj964  32219  satfvsucsuc  32616  satfrnmapom  32621  satf0op  32628  fmlaomn0  32641  dfso2  32994  soseq  33100  frrlem12  33138  lineunray  33612  bj-dfbi4  33910  poimirlem18  34914  poimirlem23  34919  poimirlem27  34923  poimirlem31  34927  itg2addnclem2  34948  tsxo1  35419  tsxo2  35420  tsxo3  35421  tsxo4  35422  tsna1  35426  tsna2  35427  tsna3  35428  ts3an1  35432  ts3an2  35433  ts3an3  35434  ts3or1  35435  ts3or2  35436  ts3or3  35437  dfeldisj5  35958  ifpim123g  39872  ifpor123g  39880  rp-fakeoranass  39886  ontric3g  39894  frege133d  40116  or3or  40377  undif3VD  41222  wallispilem3  42359  iccpartgt  43594  nnsum4primeseven  43972  nnsum4primesevenALTV  43973  lindslinindsimp2  44525