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  1534  norass  1537  cadan  1609  19.45v  1999  19.45  2239  3r19.43  3102  unass  4135  tz7.48lem  8409  dffin7-2  10351  zorng  10457  entri2  10511  grothprim  10787  leloe  11260  arch  12439  elznn0nn  12543  xrleloe  13104  swrdnnn0nd  14621  ressval3d  17216  opsrtoslem1  21962  fctop2  22892  alexsubALTlem3  23936  noextenddif  27580  sleloe  27666  precsexlem11  28119  eln0s  28251  colinearalg  28837  numclwwlk3lem2  30313  disjnf  32499  ballotlemfc0  34484  ballotlemfcc  34485  satfvsucsuc  35352  satfbrsuc  35353  fmlasuc  35373  ordcmp  36435  wl-df2-3mintru2  37473  poimirlem21  37635  ovoliunnfl  37656  biimpor  38078  tsim1  38124  leatb  39285  expdioph  43012  dflim5  43318  ifpim123g  43489  ifpimimb  43493  ifpororb  43494  rp-fakeinunass  43504  andi3or  44013  uneqsn  44014  sbc3or  44522  en3lpVD  44834  el1fzopredsuc  47323  iccpartgt  47425  fmtno4prmfac  47570  dfvopnbgr2  47850  isubgr3stgrlem4  47965  gpgprismgr4cycllem7  48088  ldepspr  48459