Theorem orbi1i 924

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

Syntax hints:   ↔ wb 208   ∨ wo 858

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 859

This theorem is referenced by:  orbi12i  925  orordi  939  3ianor  1119  3or6  1468  norasslem1  1554  norass  1557  cadan  1629  19.45v  2019  19.45  2273  3r19.43  3131  unass  4124  tz7.48lem  8412  dffin7-2  10355  zorng  10461  entri2  10515  grothprim  10792  leloe  11269  arch  12478  elznn0nn  12582  xrleloe  13146  swrdnnn0nd  14670  ressval3d  17282  opsrtoslem1  22105  fctop2  23062  alexsubALTlem3  24106  noextenddif  27729  lesloe  27815  precsexlem11  28307  eln0s  28451  bdayfinbndlem1  28557  colinearalg  29108  numclwwlk3lem2  30583  disjnf  32767  ballotlemfc0  34787  ballotlemfcc  34788  satfvsucsuc  35712  satfbrsuc  35713  fmlasuc  35733  ordcmp  36804  wl-df2-3mintru2  37976  poimirlem21  38137  ovoliunnfl  38158  biimpor  38580  tsim1  38626  leatb  39913  expdioph  43597  dflim5  43903  ifpim123g  44073  ifpimimb  44077  ifpororb  44078  rp-fakeinunass  44088  andi3or  44597  uneqsn  44598  sbc3or  45105  en3lpVD  45417  el1fzopredsuc  47917  iccpartgt  48030  fmtno4prmfac  48178  dfvopnbgr2  48472  isubgr3stgrlem4  48588  gpgprismgr4cycllem7  48720  ldepspr  49092