Theorem orbi1i 912

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

Syntax hints:   ↔ wb 206   ∨ wo 846

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 847

This theorem is referenced by:  orbi12i  913  orordi  927  3ianor  1107  3or6  1447  norasslem1  1531  norass  1534  cadan  1606  19.45v  1993  19.45  2239  unass  4195  tz7.48lem  8497  dffin7-2  10467  zorng  10573  entri2  10627  grothprim  10903  leloe  11376  arch  12550  elznn0nn  12653  xrleloe  13206  swrdnnn0nd  14704  ressval3d  17305  ressval3dOLD  17306  opsrtoslem1  22102  fctop2  23033  alexsubALTlem3  24078  noextenddif  27731  sleloe  27817  precsexlem11  28259  eln0s  28376  colinearalg  28943  numclwwlk3lem2  30416  disjnf  32592  ballotlemfc0  34457  ballotlemfcc  34458  satfvsucsuc  35333  satfbrsuc  35334  fmlasuc  35354  ordcmp  36413  wl-df2-3mintru2  37451  poimirlem21  37601  ovoliunnfl  37622  biimpor  38044  tsim1  38090  leatb  39248  metakunt1  42162  expdioph  42980  dflim5  43291  ifpim123g  43462  ifpimimb  43466  ifpororb  43467  rp-fakeinunass  43477  andi3or  43986  uneqsn  43987  sbc3or  44503  en3lpVD  44816  el1fzopredsuc  47240  iccpartgt  47301  fmtno4prmfac  47446  dfvopnbgr2  47725  ldepspr  48202