Theorem orbi2i 923

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

Syntax hints:   ↔ wb 208   ∨ wo 858

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 859

This theorem is referenced by:  orbi1i  924  orbi12i  925  orass  932  or4  937  or42  938  orordir  940  dn1  1069  dfifp6  1080  excxor  1536  nf3  1806  19.44v  2018  19.44  2272  sspsstri  4059  unass  4124  undi  4237  undif3  4252  2nreu  4398  undif4  4421  ssunpr  4792  sspr  4793  sstp  4794  pr1eqbg  4815  iinun2  5030  iinuni  5055  qfto  6108  somin1  6120  ordtri2  6381  on0eqel  6471  frxp  8106  poxp2  8123  soseq  8139  frrlem12  8278  supgtoreq  9417  wemapsolem  9498  fin1a2lem12  10368  psslinpr  10989  suplem2pr  11011  fimaxre  12136  ind1a  12206  elnn0  12483  elxnn0  12556  elnn1uz2  12926  elxr  13118  xrinfmss  13313  elfzp1  13579  hashf1lem2  14469  dvdslelem  16343  pythagtrip  16870  tosso  18449  orngsqr  20912  maducoeval2  22697  madugsum  22700  ist0-3  23402  limcdif  25935  ellimc2  25936  limcmpt  25942  limcres  25945  plydivex  26358  taylfval  26419  precsexlem9  28305  z12zsodd  28572  legtrid  28757  legso  28765  lmicom  28958  numedglnl  29342  nb3grprlem2  29579  clwwlkneq0  30228  atomli  32582  atoml2i  32583  or3di  32656  disjnf  32767  disjex  32789  disjexc  32790  cycpmrn  33320  esumcvg  34380  voliune  34523  volfiniune  34524  bnj964  35235  satfvsucsuc  35712  satfrnmapom  35717  satf0op  35724  fmlaomn0  35737  dfso2  36102  lineunray  36494  bj-dfbi4  37013  bj-axadj  37523  wl-ifpimpr  37957  wl-df4-3mintru2  37978  poimirlem18  38134  poimirlem23  38139  poimirlem27  38143  poimirlem31  38147  itg2addnclem2  38168  tsxo1  38633  tsxo2  38634  tsxo3  38635  tsxo4  38636  tsna1  38640  tsna2  38641  tsna3  38642  ts3an1  38646  ts3an2  38647  ts3an3  38648  ts3or1  38649  ts3or2  38650  ts3or3  38651  dfeldisj5  39309  aks4d1p7  42697  reelznn0nn  43080  dflim5  43903  ifpim123g  44073  ifpor123g  44081  rp-fakeoranass  44087  ontric3g  44095  frege133d  44338  or3or  44596  undif3VD  45454  wallispilem3  46638  iccpartgt  48030  nnsum4primeseven  48419  nnsum4primesevenALTV  48420  clnbupgrel  48453  usgrexmpl2trifr  48656  pg4cyclnex  48746  lindslinindsimp2  49082