Theorem orbi1i 914

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

Syntax hints:   ↔ wb 206   ∨ wo 848

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 849

This theorem is referenced by:  orbi12i  915  orordi  929  3ianor  1107  3or6  1450  norasslem1  1536  norass  1539  cadan  1611  19.45v  2001  19.45  2246  3r19.43  3107  unass  4113  tz7.48lem  8373  dffin7-2  10311  zorng  10417  entri2  10471  grothprim  10748  leloe  11223  arch  12425  elznn0nn  12529  xrleloe  13086  swrdnnn0nd  14610  ressval3d  17207  opsrtoslem1  22043  fctop2  22980  alexsubALTlem3  24024  noextenddif  27646  lesloe  27732  precsexlem11  28223  eln0s  28367  bdayfinbndlem1  28473  colinearalg  28993  numclwwlk3lem2  30469  disjnf  32655  ballotlemfc0  34653  ballotlemfcc  34654  satfvsucsuc  35563  satfbrsuc  35564  fmlasuc  35584  ordcmp  36645  wl-df2-3mintru2  37815  poimirlem21  37976  ovoliunnfl  37997  biimpor  38419  tsim1  38465  leatb  39752  expdioph  43469  dflim5  43775  ifpim123g  43945  ifpimimb  43949  ifpororb  43950  rp-fakeinunass  43960  andi3or  44469  uneqsn  44470  sbc3or  44977  en3lpVD  45289  el1fzopredsuc  47786  iccpartgt  47899  fmtno4prmfac  48047  dfvopnbgr2  48341  isubgr3stgrlem4  48457  gpgprismgr4cycllem7  48589  ldepspr  48961