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

Syntax hints:   ↔ wb 205   ∨ 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 206  df-or 847

This theorem is referenced by:  orbi12i  914  orordi  928  3ianor  1108  3or6  1448  norasslem1  1536  norass  1539  cadan  1611  19.45v  1998  19.45  2232  unass  4167  tz7.48lem  8441  dffin7-2  10393  zorng  10499  entri2  10553  grothprim  10829  leloe  11300  arch  12469  elznn0nn  12572  xrleloe  13123  swrdnnn0nd  14606  ressval3d  17191  ressval3dOLD  17192  opsrtoslem1  21616  fctop2  22508  alexsubALTlem3  23553  noextenddif  27171  sleloe  27257  precsexlem11  27666  colinearalg  28199  numclwwlk3lem2  29668  disjnf  31832  ballotlemfc0  33522  ballotlemfcc  33523  satfvsucsuc  34387  satfbrsuc  34388  fmlasuc  34408  ordcmp  35380  wl-df2-3mintru2  36414  poimirlem21  36557  ovoliunnfl  36578  biimpor  37000  tsim1  37046  leatb  38210  metakunt1  41033  expdioph  41810  dflim5  42127  ifpim123g  42299  ifpimimb  42303  ifpororb  42304  rp-fakeinunass  42314  andi3or  42823  uneqsn  42824  sbc3or  43341  en3lpVD  43654  el1fzopredsuc  46081  iccpartgt  46143  fmtno4prmfac  46288  ldepspr  47202