Theorem orbi1i 926

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

Syntax hints:   ↔ wb 209   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  orbi12i  927  orordi  941  3ianor  1122  3or6  1473  norasslem1  1561  norass  1564  cadan  1636  19.45v  2026  19.45  2280  3r19.43  3140  unass  4133  tz7.48lem  8427  dffin7-2  10381  zorng  10487  entri2  10541  grothprim  10818  leloe  11295  arch  12500  elznn0nn  12604  xrleloe  13168  swrdnnn0nd  14693  ressval3d  17305  opsrtoslem1  22174  fctop2  23130  alexsubALTlem3  24174  noextenddif  27797  lesloe  27883  precsexlem11  28375  eln0s  28519  bdayfinbndlem1  28625  colinearalg  29200  numclwwlk3lem2  30675  disjnf  32855  ballotlemfc0  34827  ballotlemfcc  34828  satfvsucsuc  35755  satfbrsuc  35756  fmlasuc  35776  ordcmp  36846  wl-df2-3mintru2  38018  poimirlem21  38179  ovoliunnfl  38200  biimpor  38622  tsim1  38668  leatb  39955  expdioph  43641  dflim5  43947  ifpim123g  44117  ifpimimb  44121  ifpororb  44122  rp-fakeinunass  44132  andi3or  44641  uneqsn  44642  sbc3or  45132  en3lpVD  45444  el1fzopredsuc  47951  iccpartgt  48064  fmtno4prmfac  48212  dfvopnbgr2  48506  isubgr3stgrlem4  48622  gpgprismgr4cycllem7  48754  ldepspr  49137