Theorem orbi1i 919

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

Syntax hints:   ↔ wb 207   ∨ wo 853

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 208  df-or 854

This theorem is referenced by:  orbi12i  920  orordi  934  3ianor  1112  3or6  1455  norasslem1  1541  norass  1544  cadan  1616  19.45v  2006  19.45  2250  3r19.43  3108  unass  4101  tz7.48lem  8370  dffin7-2  10311  zorng  10417  entri2  10471  grothprim  10748  leloe  11223  arch  12425  elznn0nn  12529  xrleloe  13086  swrdnnn0nd  14610  ressval3d  17207  opsrtoslem1  22031  fctop2  22988  alexsubALTlem3  24032  noextenddif  27650  lesloe  27736  precsexlem11  28227  eln0s  28371  bdayfinbndlem1  28477  colinearalg  28997  numclwwlk3lem2  30472  disjnf  32659  ballotlemfc0  34677  ballotlemfcc  34678  satfvsucsuc  35593  satfbrsuc  35594  fmlasuc  35614  ordcmp  36675  wl-df2-3mintru2  37847  poimirlem21  38008  ovoliunnfl  38029  biimpor  38451  tsim1  38497  leatb  39784  expdioph  43468  dflim5  43774  ifpim123g  43944  ifpimimb  43948  ifpororb  43949  rp-fakeinunass  43959  andi3or  44468  uneqsn  44469  sbc3or  44976  en3lpVD  45288  el1fzopredsuc  47789  iccpartgt  47902  fmtno4prmfac  48050  dfvopnbgr2  48344  isubgr3stgrlem4  48460  gpgprismgr4cycllem7  48592  ldepspr  48964