Theorem orbi1i 910

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

Syntax hints:   ↔ wb 208   ∨ wo 843

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 209  df-or 844

This theorem is referenced by:  orbi12i  911  orordi  925  3ianor  1103  3or6  1443  norasslem1  1530  norass  1533  cadan  1610  19.45v  2000  19.45  2240  unass  4142  tz7.48lem  8077  dffin7-2  9820  zorng  9926  entri2  9980  grothprim  10256  leloe  10727  arch  11895  elznn0nn  11996  xrleloe  12538  swrdnnn0nd  14018  ressval3d  16561  opsrtoslem1  20264  fctop2  21613  alexsubALTlem3  22657  colinearalg  26696  numclwwlk3lem2  28163  disjnf  30320  ballotlemfc0  31750  ballotlemfcc  31751  satfvsucsuc  32612  satfbrsuc  32613  fmlasuc  32633  noextenddif  33175  sleloe  33233  ordcmp  33795  poimirlem21  34928  ovoliunnfl  34949  biimpor  35377  tsim1  35423  leatb  36443  expdioph  39640  ifpim123g  39886  ifpimimb  39890  ifpororb  39891  rp-fakeinunass  39901  andi3or  40392  uneqsn  40393  sbc3or  40886  en3lpVD  41199  el1fzopredsuc  43545  iccpartgt  43607  fmtno4prmfac  43754  ldepspr  44548