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  4126  tz7.48lem  8382  dffin7-2  10320  zorng  10426  entri2  10480  grothprim  10757  leloe  11231  arch  12410  elznn0nn  12514  xrleloe  13070  swrdnnn0nd  14592  ressval3d  17185  opsrtoslem1  22022  fctop2  22961  alexsubALTlem3  24005  noextenddif  27648  lesloe  27734  precsexlem11  28225  eln0s  28369  bdayfinbndlem1  28475  colinearalg  28995  numclwwlk3lem2  30471  disjnf  32657  ballotlemfc0  34671  ballotlemfcc  34672  satfvsucsuc  35581  satfbrsuc  35582  fmlasuc  35602  ordcmp  36663  wl-df2-3mintru2  37740  poimirlem21  37892  ovoliunnfl  37913  biimpor  38335  tsim1  38381  leatb  39668  expdioph  43380  dflim5  43686  ifpim123g  43856  ifpimimb  43860  ifpororb  43861  rp-fakeinunass  43871  andi3or  44380  uneqsn  44381  sbc3or  44888  en3lpVD  45200  el1fzopredsuc  47685  iccpartgt  47787  fmtno4prmfac  47932  dfvopnbgr2  48213  isubgr3stgrlem4  48329  gpgprismgr4cycllem7  48461  ldepspr  48833