Theorem orbi1d 793

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

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

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1  794  orbi12d  795  xorbi1d  1401  eueq2dc  2950  uneq1  3324  r19.45mv  3558  rexprg  3690  rextpg  3692  swopolem  4360  sowlin  4375  onsucelsucexmidlem1  4584  onsucelsucexmid  4586  ordsoexmid  4618  isosolem  5906  acexmidlema  5948  acexmidlemb  5949  acexmidlem2  5954  acexmidlemv  5955  freceq1  6491  exmidaclem  7336  exmidac  7337  elinp  7607  prloc  7624  suplocexprlemloc  7854  ltsosr  7897  suplocsrlemb  7939  axpre-ltwlin  8016  axpre-suploclemres  8034  axpre-suploc  8035  apreap  8680  apreim  8696  sup3exmid  9050  nn01to3  9758  ltxr  9917  fzpr  10219  elfzp12  10241  lcmval  12460  lcmass  12482  isprm6  12544  lringuplu  14033  domneq0  14109  znidom  14494  dedekindeulemloc  15166  dedekindeulemeu  15169  suplociccreex  15171  dedekindicclemloc  15175  dedekindicclemeu  15178  perfectlem2  15547