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  1124  3or6  1476  norasslem1  1564  norass  1567  cadan  1639  19.45v  2029  19.45  2274  3r19.43  3134  unass  4125  tz7.48lem  8424  dffin7-2  10377  zorng  10483  entri2  10537  grothprim  10814  leloe  11291  arch  12496  elznn0nn  12600  xrleloe  13164  swrdnnn0nd  14690  ressval3d  17301  opsrtoslem1  22206  fctop2  23162  alexsubALTlem3  24206  noextenddif  27832  lesloe  27918  precsexlem11  28410  eln0s  28554  bdayfinbndlem1  28660  colinearalg  29260  numclwwlk3lem2  30735  disjnf  32915  ballotlemfc0  34883  ballotlemfcc  34884  satfvsucsuc  35857  satfbrsuc  35858  fmlasuc  35878  ordcmp  36958  wl-df2-3mintru2  38131  poimirlem21  38292  ovoliunnfl  38313  biimpor  38735  tsim1  38779  leatb  40066  expdioph  43750  dflim5  44056  ifpim123g  44226  ifpimimb  44230  ifpororb  44231  rp-fakeinunass  44241  andi3or  44750  uneqsn  44751  sbc3or  45241  en3lpVD  45553  el1fzopredsuc  48063  iccpartgt  48176  fmtno4prmfac  48324  dfvopnbgr2  48618  isubgr3stgrlem4  48734  gpgprismgr4cycllem7  48866  ldepspr  49253