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

Syntax hints:   ↔ wb 205   ∨ 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 206  df-or 844

This theorem is referenced by:  orbi1i  910  orbi12i  911  orass  918  or4  923  or42  924  orordir  926  dn1  1054  dfifp6  1065  excxor  1509  nf3  1790  nfnbiOLD  1859  19.44v  1997  19.44  2233  sspsstri  4033  unass  4096  undi  4205  undif3  4221  2nreu  4372  undif4  4397  ssunpr  4762  sspr  4763  sstp  4764  pr1eqbg  4784  iinun2  4998  iinuni  5023  qfto  6015  somin1  6027  ordtri2  6286  on0eqel  6369  frxp  7938  frrlem12  8084  wfrlem14OLD  8124  wfrlem15OLD  8125  supgtoreq  9159  wemapsolem  9239  fin1a2lem12  10098  psslinpr  10718  suplem2pr  10740  fimaxre  11849  elnn0  12165  elxnn0  12237  elnn1uz2  12594  elxr  12781  xrinfmss  12973  elfzp1  13235  hashf1lem2  14098  dvdslelem  15946  pythagtrip  16463  tosso  18052  maducoeval2  21697  madugsum  21700  ist0-3  22404  limcdif  24945  ellimc2  24946  limcmpt  24952  limcres  24955  plydivex  25362  taylfval  25423  legtrid  26856  legso  26864  lmicom  27053  numedglnl  27417  nb3grprlem2  27651  clwwlkneq0  28294  atomli  30645  atoml2i  30646  or3di  30711  disjnf  30810  disjex  30832  disjexc  30833  cycpmrn  31312  orngsqr  31405  ind1a  31887  esumcvg  31954  voliune  32097  volfiniune  32098  bnj964  32823  satfvsucsuc  33227  satfrnmapom  33232  satf0op  33239  fmlaomn0  33252  dfso2  33628  poxp2  33717  poxp3  33723  soseq  33730  lineunray  34376  bj-dfbi4  34681  wl-ifpimpr  35564  wl-df4-3mintru2  35585  poimirlem18  35722  poimirlem23  35727  poimirlem27  35731  poimirlem31  35735  itg2addnclem2  35756  tsxo1  36222  tsxo2  36223  tsxo3  36224  tsxo4  36225  tsna1  36229  tsna2  36230  tsna3  36231  ts3an1  36235  ts3an2  36236  ts3an3  36237  ts3or1  36238  ts3or2  36239  ts3or3  36240  dfeldisj5  36759  aks4d1p7  40019  ifpim123g  41005  ifpor123g  41013  rp-fakeoranass  41019  ontric3g  41027  frege133d  41262  or3or  41520  undif3VD  42391  wallispilem3  43498  iccpartgt  44767  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  lindslinindsimp2  45692