Theorem orbi1i 922

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 879	. 2 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜒 ∨ 𝜑))
2		orbi2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	2	orbi2i 921	. 2 ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))
4		orcom 879	. 2 ⊢ ((𝜒 ∨ 𝜓) ↔ (𝜓 ∨ 𝜒))
5	1, 3, 4	3bitri 299	1 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒))

Syntax hints:   ↔ wb 208   ∨ wo 856

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 209  df-or 857

This theorem is referenced by:  orbi12i  923  orordi  937  3ianor  1115  3or6  1462  norasslem1  1548  norass  1551  cadan  1623  19.45v  2013  19.45  2267  3r19.43  3125  unass  4119  tz7.48lem  8400  dffin7-2  10345  zorng  10451  entri2  10505  grothprim  10782  leloe  11259  arch  12468  elznn0nn  12572  xrleloe  13136  swrdnnn0nd  14660  ressval3d  17258  opsrtoslem1  22081  fctop2  23038  alexsubALTlem3  24082  noextenddif  27702  lesloe  27788  precsexlem11  28280  eln0s  28424  bdayfinbndlem1  28530  colinearalg  29050  numclwwlk3lem2  30525  disjnf  32712  ballotlemfc0  34744  ballotlemfcc  34745  satfvsucsuc  35663  satfbrsuc  35664  fmlasuc  35684  ordcmp  36755  wl-df2-3mintru2  37927  poimirlem21  38088  ovoliunnfl  38109  biimpor  38531  tsim1  38577  leatb  39864  expdioph  43548  dflim5  43854  ifpim123g  44024  ifpimimb  44028  ifpororb  44029  rp-fakeinunass  44039  andi3or  44548  uneqsn  44549  sbc3or  45056  en3lpVD  45368  el1fzopredsuc  47868  iccpartgt  47981  fmtno4prmfac  48129  dfvopnbgr2  48423  isubgr3stgrlem4  48539  gpgprismgr4cycllem7  48671  ldepspr  49043