Theorem orbi1i 913

Description: Inference adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.)

Hypothesis

Ref	Expression
orbi2i.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
orbi1i	⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒))

Proof of Theorem orbi1i

Step	Hyp	Ref	Expression
1		orcom 870	. 2 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜒 ∨ 𝜑))
2		orbi2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	2	orbi2i 912	. 2 ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))
4		orcom 870	. 2 ⊢ ((𝜒 ∨ 𝜓) ↔ (𝜓 ∨ 𝜒))
5	1, 3, 4	3bitri 297	1 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒))

Syntax hints:   ↔ wb 206   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  orbi12i  914  orordi  928  3ianor  1106  3or6  1448  norasslem1  1533  norass  1536  cadan  1608  19.45v  1992  19.45  2237  unass  4171  tz7.48lem  8482  dffin7-2  10439  zorng  10545  entri2  10599  grothprim  10875  leloe  11348  arch  12525  elznn0nn  12629  xrleloe  13187  swrdnnn0nd  14695  ressval3d  17293  opsrtoslem1  22080  fctop2  23013  alexsubALTlem3  24058  noextenddif  27714  sleloe  27800  precsexlem11  28242  eln0s  28359  colinearalg  28926  numclwwlk3lem2  30404  disjnf  32584  ballotlemfc0  34496  ballotlemfcc  34497  satfvsucsuc  35371  satfbrsuc  35372  fmlasuc  35392  ordcmp  36449  wl-df2-3mintru2  37487  poimirlem21  37649  ovoliunnfl  37670  biimpor  38092  tsim1  38138  leatb  39294  metakunt1  42207  expdioph  43040  dflim5  43347  ifpim123g  43518  ifpimimb  43522  ifpororb  43523  rp-fakeinunass  43533  andi3or  44042  uneqsn  44043  sbc3or  44557  en3lpVD  44870  el1fzopredsuc  47342  iccpartgt  47419  fmtno4prmfac  47564  dfvopnbgr2  47844  isubgr3stgrlem4  47941  ldepspr  48395