Theorem orbi1i 927

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

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  orbi12i  928  orordi  942  3ianor  1124  3or6  1476  norasslem1  1564  norass  1567  cadan  1642  19.45v  2032  19.45  2277  3r19.43  3136  unass  4125  tz7.48lem  8434  dffin7-2  10397  zorng  10503  entri2  10557  grothprim  10834  leloe  11311  arch  12516  elznn0nn  12620  xrleloe  13185  swrdnnn0nd  14716  ressval3d  17328  opsrtoslem1  22256  fctop2  23212  alexsubALTlem3  24257  noextenddif  27883  lesloe  27969  precsexlem11  28461  eln0s  28605  bdayfinbndlem1  28711  colinearalg  29315  numclwwlk3lem2  30806  disjnf  32986  ballotlemfc0  34948  ballotlemfcc  34949  satfvsucsuc  35894  satfbrsuc  35895  fmlasuc  35915  ordcmp  37015  wl-df2-3mintru2  38188  poimirlem21  38349  ovoliunnfl  38370  biimpor  38793  tsim1  38837  leatb  40124  expdioph  43808  dflim5  44114  ifpim123g  44284  ifpimimb  44288  ifpororb  44289  rp-fakeinunass  44299  andi3or  44808  uneqsn  44809  sbc3or  45299  en3lpVD  45611  el1fzopredsuc  48121  iccpartgt  48234  fmtno4prmfac  48382  dfvopnbgr2  48676  isubgr3stgrlem4  48792  gpgprismgr4cycllem7  48924  ldepspr  49310