Theorem orbi1i 944

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

Syntax hints:   ↔ wb 198   ∨ wo 880

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 199  df-or 881

This theorem is referenced by:  orbi12i  945  orordi  959  3anorOLD  1136  3ianor  1138  3or6  1577  cadan  1724  nfnbiOLD  1957  19.45v  2101  19.45  2284  unass  3998  tz7.48lem  7803  dffin7-2  9536  zorng  9642  entri2  9696  grothprim  9972  leloe  10444  arch  11616  elznn0nn  11719  xrleloe  12264  swrdnnn0nd  13722  ressval3d  16301  ressval3dOLD  16302  opsrtoslem1  19845  fctop2  21181  alexsubALTlem3  22224  colinearalg  26210  numclwwlk3lem2  27800  disjnf  29932  ballotlemfc0  31101  ballotlemfcc  31102  noextenddif  32361  sleloe  32419  ordcmp  32980  poimirlem21  33975  ovoliunnfl  33996  biimpor  34426  tsim1  34478  leatb  35368  expdioph  38434  ifpim123g  38688  ifpimimb  38692  ifpororb  38693  rp-fakeinunass  38703  andi3or  39161  uneqsn  39162  sbc3or  39577  en3lpVD  39900  el1fzopredsuc  42224  iccpartgt  42252  fmtno4prmfac  42315  ldepspr  43110