Theorem orbi1i 927

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 884	. 2 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜒 ∨ 𝜑))
2		orbi2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	2	orbi2i 926	. 2 ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))
4		orcom 884	. 2 ⊢ ((𝜒 ∨ 𝜓) ↔ (𝜓 ∨ 𝜒))
5	1, 3, 4	3bitri 300	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:  orbi12i  928  orordi  942  3ianor  1124  3or6  1476  norasslem1  1564  norass  1567  cadan  1642  19.45v  2032  19.45  2274  3r19.43  3131  unass  4118  tz7.48lem  8430  dffin7-2  10400  zorng  10506  entri2  10566  grothprim  10843  leloe  11320  arch  12525  elznn0nn  12629  xrleloe  13195  swrdnnn0nd  14726  ressval3d  17338  opsrtoslem1  22271  fctop2  23230  alexsubALTlem3  24275  noextenddif  27904  lesloe  27990  precsexlem11  28482  eln0s  28626  bdayfinbndlem1  28732  colinearalg  29367  numclwwlk3lem2  30864  disjnf  33043  ballotlemfc0  35004  ballotlemfcc  35005  satfvsucsuc  35944  satfbrsuc  35945  fmlasuc  35965  ordcmp  37066  wl-df2-3mintru2  38239  poimirlem21  38390  ovoliunnfl  38411  biimpor  38834  tsim1  38878  leatb  40165  expdioph  43864  dflim5  44170  ifpim123g  44340  ifpimimb  44344  ifpororb  44345  rp-fakeinunass  44355  andi3or  44864  uneqsn  44865  sbc3or  45355  en3lpVD  45667  el1fzopredsuc  48214  iccpartgt  48327  fmtno4prmfac  48475  dfvopnbgr2  48769  isubgr3stgrlem4  48885  gpgprismgr4cycllem7  49017  ldepspr  49403