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  1563  norass  1566  cadan  1641  19.45v  2031  19.45  2274  3r19.43  3131  unass  4169  tz7.48lemOLD  8458  dffin7-2  10483  zorng  10589  entri2  10649  grothprim  10926  leloe  11403  arch  12610  elznn0nn  12714  xrleloe  13280  swrdnnn0nd  14814  ressval3d  17433  opsrtoslem1  22373  fctop2  23332  alexsubALTlem3  24377  noextenddif  28034  lesloe  28120  precsexlem11  28612  eln0s  28756  bdayfinbndlem1  28862  colinearalg  29497  numclwwlk3lem2  30994  disjnf  33215  ballotlemfc0  35175  ballotlemfcc  35176  werankwe  35795  werankwe2  35796  satfvsucsuc  36220  satfbrsuc  36221  fmlasuc  36241  ordcmp  37331  wl-df2-3mintru2  38517  poimirlem21  38668  ovoliunnfl  38689  biimpor  39127  tsim1  39171  leatb  40458  expdioph  44139  dflim5  44440  ifpim123g  44610  ifpimimb  44614  ifpororb  44615  rp-fakeinunass  44625  andi3or  45133  uneqsn  45134  sbc3or  45623  en3lpVD  45935  el1fzopredsuc  48504  iccpartgt  48617  fmtno4prmfac  48765  dfvopnbgr2  49059  isubgr3stgrlem4  49175  gpgprismgr4cycllem7  49307  ldepspr  49693