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  2275  3r19.43  3132  unass  4118  tz7.48lemOLD  8444  dffin7-2  10469  zorng  10575  entri2  10635  grothprim  10912  leloe  11389  arch  12596  elznn0nn  12700  xrleloe  13266  swrdnnn0nd  14799  ressval3d  17417  opsrtoslem1  22357  fctop2  23316  alexsubALTlem3  24361  noextenddif  28018  lesloe  28104  precsexlem11  28596  eln0s  28740  bdayfinbndlem1  28846  colinearalg  29481  numclwwlk3lem2  30978  disjnf  33157  ballotlemfc0  35118  ballotlemfcc  35119  satfvsucsuc  36109  satfbrsuc  36110  fmlasuc  36130  ordcmp  37215  wl-df2-3mintru2  38388  poimirlem21  38539  ovoliunnfl  38560  biimpor  38998  tsim1  39042  leatb  40329  expdioph  44009  dflim5  44315  ifpim123g  44485  ifpimimb  44489  ifpororb  44490  rp-fakeinunass  44500  andi3or  45009  uneqsn  45010  sbc3or  45500  en3lpVD  45812  el1fzopredsuc  48365  iccpartgt  48478  fmtno4prmfac  48626  dfvopnbgr2  48920  isubgr3stgrlem4  49036  gpgprismgr4cycllem7  49168  ldepspr  49554