Theorem orbi1i 937

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

Syntax hints:   ↔ wb 197   ∨ wo 873

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 198  df-or 874

This theorem is referenced by:  orbi12i  938  orordi  952  3anorOLD  1130  3ianor  1132  3or6  1571  cadan  1718  nfnbiOLD  1951  19.45v  2093  19.45  2272  unass  3931  tz7.48lem  7739  dffin7-2  9472  zorng  9578  entri2  9632  grothprim  9908  leloe  10377  arch  11534  elznn0nn  11637  xrleloe  12176  ressval3d  16210  ressval3dOLD  16211  opsrtoslem1  19756  fctop2  21088  alexsubALTlem3  22131  colinearalg  26080  numclwwlk3lem2  27634  disjnf  29766  ballotlemfc0  30936  ballotlemfcc  30937  noextenddif  32196  sleloe  32254  ordcmp  32816  poimirlem21  33786  ovoliunnfl  33807  biimpor  34237  tsim1  34290  leatb  35180  expdioph  38199  ifpim123g  38453  ifpimimb  38457  ifpororb  38458  rp-fakeinunass  38468  andi3or  38926  uneqsn  38927  sbc3or  39342  en3lpVD  39665  el1fzopredsuc  42001  iccpartgt  42029  fmtno4prmfac  42092  ldepspr  42863