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

Syntax hints:   ↔ wb 205   ∨ wo 845

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 206  df-or 846

This theorem is referenced by:  orbi12i  913  orordi  927  3ianor  1107  3or6  1447  norasslem1  1535  norass  1538  cadan  1610  19.45v  1997  19.45  2231  unass  4166  tz7.48lem  8440  dffin7-2  10392  zorng  10498  entri2  10552  grothprim  10828  leloe  11299  arch  12468  elznn0nn  12571  xrleloe  13122  swrdnnn0nd  14605  ressval3d  17190  ressval3dOLD  17191  opsrtoslem1  21615  fctop2  22507  alexsubALTlem3  23552  noextenddif  27168  sleloe  27254  precsexlem11  27660  colinearalg  28165  numclwwlk3lem2  29634  disjnf  31796  ballotlemfc0  33486  ballotlemfcc  33487  satfvsucsuc  34351  satfbrsuc  34352  fmlasuc  34372  ordcmp  35327  wl-df2-3mintru2  36361  poimirlem21  36504  ovoliunnfl  36525  biimpor  36947  tsim1  36993  leatb  38157  metakunt1  40980  expdioph  41752  dflim5  42069  ifpim123g  42241  ifpimimb  42245  ifpororb  42246  rp-fakeinunass  42256  andi3or  42765  uneqsn  42766  sbc3or  43283  en3lpVD  43596  el1fzopredsuc  46023  iccpartgt  46085  fmtno4prmfac  46230  ldepspr  47144