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  1449  norasslem1  1535  norass  1538  cadan  1610  19.45v  2000  19.45  2243  3r19.43  3103  unass  4122  tz7.48lem  8370  dffin7-2  10306  zorng  10412  entri2  10466  grothprim  10743  leloe  11217  arch  12396  elznn0nn  12500  xrleloe  13056  swrdnnn0nd  14578  ressval3d  17171  opsrtoslem1  22008  fctop2  22947  alexsubALTlem3  23991  noextenddif  27634  sleloe  27720  precsexlem11  28185  eln0s  28320  colinearalg  28932  numclwwlk3lem2  30408  disjnf  32594  ballotlemfc0  34599  ballotlemfcc  34600  satfvsucsuc  35508  satfbrsuc  35509  fmlasuc  35529  ordcmp  36590  wl-df2-3mintru2  37629  poimirlem21  37781  ovoliunnfl  37802  biimpor  38224  tsim1  38270  leatb  39491  expdioph  43207  dflim5  43513  ifpim123g  43683  ifpimimb  43687  ifpororb  43688  rp-fakeinunass  43698  andi3or  44207  uneqsn  44208  sbc3or  44715  en3lpVD  45027  el1fzopredsuc  47513  iccpartgt  47615  fmtno4prmfac  47760  dfvopnbgr2  48041  isubgr3stgrlem4  48157  gpgprismgr4cycllem7  48289  ldepspr  48661