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  3106  unass  4112  tz7.48lem  8380  dffin7-2  10320  zorng  10426  entri2  10480  grothprim  10757  leloe  11232  arch  12434  elznn0nn  12538  xrleloe  13095  swrdnnn0nd  14619  ressval3d  17216  opsrtoslem1  22033  fctop2  22970  alexsubALTlem3  24014  noextenddif  27632  lesloe  27718  precsexlem11  28209  eln0s  28353  bdayfinbndlem1  28459  colinearalg  28979  numclwwlk3lem2  30454  disjnf  32640  ballotlemfc0  34637  ballotlemfcc  34638  satfvsucsuc  35547  satfbrsuc  35548  fmlasuc  35568  ordcmp  36629  wl-df2-3mintru2  37801  poimirlem21  37962  ovoliunnfl  37983  biimpor  38405  tsim1  38451  leatb  39738  expdioph  43451  dflim5  43757  ifpim123g  43927  ifpimimb  43931  ifpororb  43932  rp-fakeinunass  43942  andi3or  44451  uneqsn  44452  sbc3or  44959  en3lpVD  45271  el1fzopredsuc  47774  iccpartgt  47887  fmtno4prmfac  48035  dfvopnbgr2  48329  isubgr3stgrlem4  48445  gpgprismgr4cycllem7  48577  ldepspr  48949