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  1534  norass  1537  cadan  1609  19.45v  1999  19.45  2239  3r19.43  3098  unass  4123  tz7.48lem  8363  dffin7-2  10292  zorng  10398  entri2  10452  grothprim  10728  leloe  11202  arch  12381  elznn0nn  12485  xrleloe  13046  swrdnnn0nd  14563  ressval3d  17157  opsrtoslem1  21960  fctop2  22890  alexsubALTlem3  23934  noextenddif  27578  sleloe  27664  precsexlem11  28124  eln0s  28256  colinearalg  28855  numclwwlk3lem2  30328  disjnf  32514  ballotlemfc0  34461  ballotlemfcc  34462  satfvsucsuc  35338  satfbrsuc  35339  fmlasuc  35359  ordcmp  36421  wl-df2-3mintru2  37459  poimirlem21  37621  ovoliunnfl  37642  biimpor  38064  tsim1  38110  leatb  39271  expdioph  42996  dflim5  43302  ifpim123g  43473  ifpimimb  43477  ifpororb  43478  rp-fakeinunass  43488  andi3or  43997  uneqsn  43998  sbc3or  44506  en3lpVD  44818  el1fzopredsuc  47309  iccpartgt  47411  fmtno4prmfac  47556  dfvopnbgr2  47837  isubgr3stgrlem4  47953  gpgprismgr4cycllem7  48085  ldepspr  48458