Theorem orbi2i 910

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

Syntax hints:   ↔ wb 205   ∨ wo 845

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 846

This theorem is referenced by:  orbi1i  911  orbi12i  912  orass  919  or4  924  or42  925  orordir  927  dn1  1055  dfifp6  1066  excxor  1510  nf3  1781  nfnbiOLD  1851  19.44v  1989  19.44  2226  sspsstri  4098  unass  4164  undi  4273  undif3  4289  2nreu  4438  undif4  4461  ssunpr  4833  sspr  4834  sstp  4835  pr1eqbg  4855  iinun2  5073  iinuni  5098  qfto  6125  somin1  6137  ordtri2  6403  on0eqel  6492  frxp  8132  poxp2  8149  soseq  8165  frrlem12  8304  wfrlem14OLD  8344  wfrlem15OLD  8345  supgtoreq  9506  wemapsolem  9586  fin1a2lem12  10445  psslinpr  11065  suplem2pr  11087  fimaxre  12204  elnn0  12520  elxnn0  12592  elnn1uz2  12955  elxr  13144  xrinfmss  13337  elfzp1  13599  hashf1lem2  14470  dvdslelem  16306  pythagtrip  16831  tosso  18439  maducoeval2  22630  madugsum  22633  ist0-3  23337  limcdif  25893  ellimc2  25894  limcmpt  25900  limcres  25903  plydivex  26322  taylfval  26383  precsexlem9  28211  legtrid  28515  legso  28523  lmicom  28712  numedglnl  29077  nb3grprlem2  29314  clwwlkneq0  29959  atomli  32312  atoml2i  32313  or3di  32386  disjnf  32490  disjex  32512  disjexc  32513  cycpmrn  33025  orngsqr  33187  ind1a  33865  esumcvg  33932  voliune  34075  volfiniune  34076  bnj964  34801  satfvsucsuc  35206  satfrnmapom  35211  satf0op  35218  fmlaomn0  35231  dfso2  35590  lineunray  35984  bj-dfbi4  36290  bj-axadj  36761  wl-ifpimpr  37186  wl-df4-3mintru2  37207  poimirlem18  37352  poimirlem23  37357  poimirlem27  37361  poimirlem31  37365  itg2addnclem2  37386  tsxo1  37851  tsxo2  37852  tsxo3  37853  tsxo4  37854  tsna1  37858  tsna2  37859  tsna3  37860  ts3an1  37864  ts3an2  37865  ts3an3  37866  ts3or1  37867  ts3or2  37868  ts3or3  37869  dfeldisj5  38432  aks4d1p7  41795  reelznn0nn  42160  dflim5  43032  ifpim123g  43204  ifpor123g  43212  rp-fakeoranass  43218  ontric3g  43226  frege133d  43469  or3or  43727  undif3VD  44595  wallispilem3  45724  iccpartgt  47035  nnsum4primeseven  47408  nnsum4primesevenALTV  47409  clnbupgrel  47441  lindslinindsimp2  47882