Theorem orbi1d 792

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 791	. 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒)))
3		orcom 729	. 2 ⊢ ((𝜓 ∨ 𝜃) ↔ (𝜃 ∨ 𝜓))
4		orcom 729	. 2 ⊢ ((𝜒 ∨ 𝜃) ↔ (𝜃 ∨ 𝜒))
5	2, 3, 4	3bitr4g 223	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃)))

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

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1  793  orbi12d  794  xorbi1d  1400  eueq2dc  2945  uneq1  3319  r19.45mv  3553  rexprg  3684  rextpg  3686  swopolem  4350  sowlin  4365  onsucelsucexmidlem1  4574  onsucelsucexmid  4576  ordsoexmid  4608  isosolem  5883  acexmidlema  5925  acexmidlemb  5926  acexmidlem2  5931  acexmidlemv  5932  freceq1  6468  exmidaclem  7302  exmidac  7303  elinp  7569  prloc  7586  suplocexprlemloc  7816  ltsosr  7859  suplocsrlemb  7901  axpre-ltwlin  7978  axpre-suploclemres  7996  axpre-suploc  7997  apreap  8642  apreim  8658  sup3exmid  9012  nn01to3  9720  ltxr  9879  fzpr  10181  elfzp12  10203  lcmval  12304  lcmass  12326  isprm6  12388  lringuplu  13876  domneq0  13952  znidom  14337  dedekindeulemloc  15009  dedekindeulemeu  15012  suplociccreex  15014  dedekindicclemloc  15018  dedekindicclemeu  15021  perfectlem2  15390