Theorem orbi1d 799

Description: Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.)

Hypothesis

Ref	Expression
orbid.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
orbi1d	⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃)))

Proof of Theorem orbi1d

Step	Hyp	Ref	Expression
1		orbid.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	orbi2d 798	. 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒)))
3		orcom 736	. 2 ⊢ ((𝜓 ∨ 𝜃) ↔ (𝜃 ∨ 𝜓))
4		orcom 736	. 2 ⊢ ((𝜒 ∨ 𝜃) ↔ (𝜃 ∨ 𝜒))
5	2, 3, 4	3bitr4g 223	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 105   ∨ wo 716

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1  800  orbi12d  801  xorbi1d  1426  eueq2dc  2980  uneq1  3356  r19.45mv  3590  rexprg  3725  rextpg  3727  swopolem  4408  sowlin  4423  onsucelsucexmidlem1  4632  onsucelsucexmid  4634  ordsoexmid  4666  isosolem  5975  acexmidlema  6019  acexmidlemb  6020  acexmidlem2  6025  acexmidlemv  6026  freceq1  6601  exmidaclem  7466  exmidac  7467  elinp  7737  prloc  7754  suplocexprlemloc  7984  ltsosr  8027  suplocsrlemb  8069  axpre-ltwlin  8146  axpre-suploclemres  8164  axpre-suploc  8165  apreap  8809  apreim  8825  sup3exmid  9179  nn01to3  9895  ltxr  10054  fzpr  10357  elfzp12  10379  lcmval  12698  lcmass  12720  isprm6  12782  lringuplu  14274  domneq0  14351  znidom  14736  dedekindeulemloc  15413  dedekindeulemeu  15416  suplociccreex  15418  dedekindicclemloc  15422  dedekindicclemeu  15425  perfectlem2  15797