Theorem orbi1i 911

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

Syntax hints:   ↔ wb 209   ∨ wo 844

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 210  df-or 845

This theorem is referenced by:  orbi12i  912  orordi  926  3ianor  1104  3or6  1444  norasslem1  1531  norass  1534  cadan  1611  19.45v  2000  19.45  2238  unass  4093  tz7.48lem  8060  dffin7-2  9809  zorng  9915  entri2  9969  grothprim  10245  leloe  10716  arch  11882  elznn0nn  11983  xrleloe  12525  swrdnnn0nd  14009  ressval3d  16553  opsrtoslem1  20723  fctop2  21610  alexsubALTlem3  22654  colinearalg  26704  numclwwlk3lem2  28169  disjnf  30333  ballotlemfc0  31860  ballotlemfcc  31861  satfvsucsuc  32725  satfbrsuc  32726  fmlasuc  32746  noextenddif  33288  sleloe  33346  ordcmp  33908  wl-df2-3mintru2  34902  poimirlem21  35078  ovoliunnfl  35099  biimpor  35522  tsim1  35568  leatb  36588  metakunt1  39350  expdioph  39964  ifpim123g  40208  ifpimimb  40212  ifpororb  40213  rp-fakeinunass  40223  andi3or  40725  uneqsn  40726  sbc3or  41238  en3lpVD  41551  el1fzopredsuc  43882  iccpartgt  43944  fmtno4prmfac  44089  ldepspr  44882