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  1513  nf3  1786  nfnbiOLD  1856  19.44v  1994  19.44  2228  sspsstri  4103  unass  4167  undi  4275  undif3  4291  2nreu  4442  undif4  4467  ssunpr  4836  sspr  4837  sstp  4838  pr1eqbg  4858  iinun2  5077  iinuni  5102  qfto  6123  somin1  6135  ordtri2  6400  on0eqel  6489  frxp  8116  poxp2  8133  soseq  8149  frrlem12  8286  wfrlem14OLD  8326  wfrlem15OLD  8327  supgtoreq  9469  wemapsolem  9549  fin1a2lem12  10410  psslinpr  11030  suplem2pr  11052  fimaxre  12164  elnn0  12480  elxnn0  12552  elnn1uz2  12915  elxr  13102  xrinfmss  13295  elfzp1  13557  hashf1lem2  14423  dvdslelem  16258  pythagtrip  16773  tosso  18378  maducoeval2  22364  madugsum  22367  ist0-3  23071  limcdif  25627  ellimc2  25628  limcmpt  25634  limcres  25637  plydivex  26044  taylfval  26105  precsexlem9  27898  legtrid  28107  legso  28115  lmicom  28304  numedglnl  28669  nb3grprlem2  28903  clwwlkneq0  29547  atomli  31900  atoml2i  31901  or3di  31966  disjnf  32066  disjex  32088  disjexc  32089  cycpmrn  32570  orngsqr  32690  ind1a  33313  esumcvg  33380  voliune  33523  volfiniune  33524  bnj964  34250  satfvsucsuc  34652  satfrnmapom  34657  satf0op  34664  fmlaomn0  34677  dfso2  35027  lineunray  35421  bj-dfbi4  35755  bj-axadj  36227  wl-ifpimpr  36652  wl-df4-3mintru2  36673  poimirlem18  36811  poimirlem23  36816  poimirlem27  36820  poimirlem31  36824  itg2addnclem2  36845  tsxo1  37310  tsxo2  37311  tsxo3  37312  tsxo4  37313  tsna1  37317  tsna2  37318  tsna3  37319  ts3an1  37323  ts3an2  37324  ts3an3  37325  ts3or1  37326  ts3or2  37327  ts3or3  37328  dfeldisj5  37896  aks4d1p7  41256  reelznn0nn  41626  dflim5  42383  ifpim123g  42555  ifpor123g  42563  rp-fakeoranass  42569  ontric3g  42577  frege133d  42820  or3or  43078  undif3VD  43947  wallispilem3  45083  iccpartgt  46395  nnsum4primeseven  46768  nnsum4primesevenALTV  46769  lindslinindsimp2  47233