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  3110  unass  4152  tz7.48lem  8460  dffin7-2  10417  zorng  10523  entri2  10577  grothprim  10853  leloe  11326  arch  12503  elznn0nn  12607  xrleloe  13165  swrdnnn0nd  14679  ressval3d  17272  opsrtoslem1  22018  fctop2  22948  alexsubALTlem3  23992  noextenddif  27637  sleloe  27723  precsexlem11  28176  eln0s  28308  colinearalg  28894  numclwwlk3lem2  30370  disjnf  32556  ballotlemfc0  34530  ballotlemfcc  34531  satfvsucsuc  35392  satfbrsuc  35393  fmlasuc  35413  ordcmp  36470  wl-df2-3mintru2  37508  poimirlem21  37670  ovoliunnfl  37691  biimpor  38113  tsim1  38159  leatb  39315  expdioph  43014  dflim5  43320  ifpim123g  43491  ifpimimb  43495  ifpororb  43496  rp-fakeinunass  43506  andi3or  44015  uneqsn  44016  sbc3or  44524  en3lpVD  44836  el1fzopredsuc  47321  iccpartgt  47408  fmtno4prmfac  47553  dfvopnbgr2  47833  isubgr3stgrlem4  47948  gpgprismgr4cycllem7  48067  ldepspr  48416