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  1477  norasslem1  1564  norass  1567  cadan  1642  19.45v  2034  19.45  2278  3r19.43  3135  unass  4173  tz7.48lemOLD  8489  dffin7-2  10515  zorng  10621  entri2  10681  grothprim  10958  leloe  11435  arch  12643  elznn0nn  12747  xrleloe  13313  swrdnnn0nd  14848  ressval3d  17468  opsrtoslem1  22419  fctop2  23378  alexsubALTlem3  24423  noextenddif  28082  lesloe  28168  precsexlem11  28660  eln0s  28804  bdayfinbndlem1  28910  colinearalg  29545  numclwwlk3lem2  31042  disjnf  33262  ballotlemfc0  35236  ballotlemfcc  35237  werankwe  35862  werankwe2  35863  satfvsucsuc  36338  satfbrsuc  36339  fmlasuc  36359  ordcmp  37450  wl-df2-3mintru2  38676  poimirlem21  38827  ovoliunnfl  38848  biimpor  39284  tsim1  39328  leatb  40615  expdioph  44296  dflim5  44592  ifpim123g  44762  ifpimimb  44766  ifpororb  44767  rp-fakeinunass  44777  andi3or  45285  uneqsn  45286  sbc3or  45775  en3lpVD  46087  el1fzopredsuc  48669  iccpartgt  48782  fmtno4prmfac  48930  dfvopnbgr2  49224  isubgr3stgrlem4  49340  gpgprismgr4cycllem7  49472  ldepspr  49916