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 297	1 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒))

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

This theorem is referenced by:  orbi12i  912  orordi  926  3ianor  1106  3or6  1446  norasslem1  1532  norass  1535  cadan  1611  19.45v  1997  19.45  2231  unass  4100  tz7.48lem  8272  dffin7-2  10154  zorng  10260  entri2  10314  grothprim  10590  leloe  11061  arch  12230  elznn0nn  12333  xrleloe  12878  swrdnnn0nd  14369  ressval3d  16956  ressval3dOLD  16957  opsrtoslem1  21262  fctop2  22155  alexsubALTlem3  23200  colinearalg  27278  numclwwlk3lem2  28748  disjnf  30909  ballotlemfc0  32459  ballotlemfcc  32460  satfvsucsuc  33327  satfbrsuc  33328  fmlasuc  33348  otthne  33682  noextenddif  33871  sleloe  33957  ordcmp  34636  wl-df2-3mintru2  35656  poimirlem21  35798  ovoliunnfl  35819  biimpor  36242  tsim1  36288  leatb  37306  metakunt1  40125  expdioph  40845  ifpim123g  41107  ifpimimb  41111  ifpororb  41112  rp-fakeinunass  41122  andi3or  41632  uneqsn  41633  sbc3or  42152  en3lpVD  42465  el1fzopredsuc  44817  iccpartgt  44879  fmtno4prmfac  45024  ldepspr  45814