Theorem orbi1i 913

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

Syntax hints:   ↔ wb 206   ∨ wo 847

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 848

This theorem is referenced by:  orbi12i  914  orordi  928  3ianor  1106  3or6  1446  norasslem1  1531  norass  1534  cadan  1606  19.45v  1991  19.45  2236  unass  4182  tz7.48lem  8480  dffin7-2  10436  zorng  10542  entri2  10596  grothprim  10872  leloe  11345  arch  12521  elznn0nn  12625  xrleloe  13183  swrdnnn0nd  14691  ressval3d  17292  ressval3dOLD  17293  opsrtoslem1  22097  fctop2  23028  alexsubALTlem3  24073  noextenddif  27728  sleloe  27814  precsexlem11  28256  eln0s  28373  colinearalg  28940  numclwwlk3lem2  30413  disjnf  32590  ballotlemfc0  34474  ballotlemfcc  34475  satfvsucsuc  35350  satfbrsuc  35351  fmlasuc  35371  ordcmp  36430  wl-df2-3mintru2  37468  poimirlem21  37628  ovoliunnfl  37649  biimpor  38071  tsim1  38117  leatb  39274  metakunt1  42187  expdioph  43012  dflim5  43319  ifpim123g  43490  ifpimimb  43494  ifpororb  43495  rp-fakeinunass  43505  andi3or  44014  uneqsn  44015  sbc3or  44530  en3lpVD  44843  el1fzopredsuc  47275  iccpartgt  47352  fmtno4prmfac  47497  dfvopnbgr2  47777  isubgr3stgrlem4  47872  ldepspr  48319