Theorem orbi1i 913

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

Syntax hints:   ↔ wb 206   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  orbi12i  914  orordi  928  3ianor  1106  3or6  1449  norasslem1  1535  norass  1538  cadan  1610  19.45v  2000  19.45  2241  3r19.43  3101  unass  4117  tz7.48lem  8355  dffin7-2  10284  zorng  10390  entri2  10444  grothprim  10720  leloe  11194  arch  12373  elznn0nn  12477  xrleloe  13038  swrdnnn0nd  14559  ressval3d  17152  opsrtoslem1  21985  fctop2  22915  alexsubALTlem3  23959  noextenddif  27602  sleloe  27688  precsexlem11  28150  eln0s  28282  colinearalg  28883  numclwwlk3lem2  30356  disjnf  32542  ballotlemfc0  34498  ballotlemfcc  34499  satfvsucsuc  35401  satfbrsuc  35402  fmlasuc  35422  ordcmp  36481  wl-df2-3mintru2  37519  poimirlem21  37681  ovoliunnfl  37702  biimpor  38124  tsim1  38170  leatb  39331  expdioph  43056  dflim5  43362  ifpim123g  43533  ifpimimb  43537  ifpororb  43538  rp-fakeinunass  43548  andi3or  44057  uneqsn  44058  sbc3or  44565  en3lpVD  44877  el1fzopredsuc  47356  iccpartgt  47458  fmtno4prmfac  47603  dfvopnbgr2  47884  isubgr3stgrlem4  48000  gpgprismgr4cycllem7  48132  ldepspr  48505