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 868	. 2 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜒 ∨ 𝜑))
2		orbi2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	2	orbi2i 910	. 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  912  orordi  926  3ianor  1104  3or6  1443  norasslem1  1527  norass  1530  cadan  1602  19.45v  1989  19.45  2226  unass  4164  tz7.48lem  8462  dffin7-2  10423  zorng  10529  entri2  10583  grothprim  10859  leloe  11332  arch  12502  elznn0nn  12605  xrleloe  13158  swrdnnn0nd  14642  ressval3d  17230  ressval3dOLD  17231  opsrtoslem1  22021  fctop2  22952  alexsubALTlem3  23997  noextenddif  27647  sleloe  27733  precsexlem11  28165  eln0s  28273  colinearalg  28793  numclwwlk3lem2  30266  disjnf  32439  ballotlemfc0  34243  ballotlemfcc  34244  satfvsucsuc  35106  satfbrsuc  35107  fmlasuc  35127  ordcmp  36062  wl-df2-3mintru2  37095  poimirlem21  37245  ovoliunnfl  37266  biimpor  37688  tsim1  37734  leatb  38894  metakunt1  41791  expdioph  42586  dflim5  42900  ifpim123g  43072  ifpimimb  43076  ifpororb  43077  rp-fakeinunass  43087  andi3or  43596  uneqsn  43597  sbc3or  44113  en3lpVD  44426  el1fzopredsuc  46843  iccpartgt  46904  fmtno4prmfac  47049  dfvopnbgr2  47325  ldepspr  47727