Theorem orbi2i 926

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

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  orbi1i  927  orbi12i  928  orass  935  or4  940  or42  941  orordir  943  dn1  1073  dfifp6  1084  excxor  1546  nf3  1819  19.44v  2031  19.44  2276  sspsstri  4061  unass  4125  undi  4238  undif3  4253  2nreu  4409  undif4  4427  ssunpr  4801  sspr  4802  sstp  4803  pr1eqbg  4824  iinun2  5039  iinuni  5066  qfto  6123  somin1  6135  ordtri2  6400  on0eqel  6490  frxp  8128  poxp2  8145  soseq  8161  frrlem12  8300  supgtoreq  9438  wemapsolem  9519  fin1a2lem12  10410  psslinpr  11031  suplem2pr  11053  fimaxre  12174  ind1a  12244  elnn0  12521  elxnn0  12594  elnn1uz2  12965  elxr  13157  xrinfmss  13352  elfzp1  13619  hashf1lem2  14511  dvdslelem  16389  pythagtrip  16916  tosso  18495  orngsqr  21019  maducoeval2  22847  madugsum  22850  ist0-3  23552  limcdif  26086  ellimc2  26087  limcmpt  26093  limcres  26096  plydivex  26509  taylfval  26573  precsexlem9  28459  z12zsodd  28726  legtrid  28911  legso  28919  lmicom  29148  numedglnl  29549  nb3grprlem2  29789  clwwlkneq0  30447  atomli  32805  atoml2i  32806  or3di  32878  disjnf  32986  disjex  33008  disjexc  33009  cycpmrn  33527  esumcvg  34540  voliune  34684  volfiniune  34685  bnj964  35396  satfvsucsuc  35894  satfrnmapom  35899  satf0op  35906  fmlaomn0  35919  dfso2  36284  lineunray  36676  bj-dfbi4  37223  bj-axadj  37734  wl-ifpimpr  38169  wl-df4-3mintru2  38190  poimirlem18  38346  poimirlem23  38351  poimirlem27  38355  poimirlem31  38359  itg2addnclem2  38380  tsxo1  38844  tsxo2  38845  tsxo3  38846  tsxo4  38847  tsna1  38851  tsna2  38852  tsna3  38853  ts3an1  38857  ts3an2  38858  ts3an3  38859  ts3or1  38860  ts3or2  38861  ts3or3  38862  dfeldisj5  39520  aks4d1p7  42908  reelznn0nn  43293  dflim5  44114  ifpim123g  44284  ifpor123g  44292  rp-fakeoranass  44298  ontric3g  44306  frege133d  44549  or3or  44807  undif3VD  45648  wallispilem3  46839  iccpartgt  48234  nnsum4primeseven  48623  nnsum4primesevenALTV  48624  clnbupgrel  48657  usgrexmpl2trifr  48860  pg4cyclnex  48950  lindslinindsimp2  49300