Theorem orbi1d 796

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

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

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1  797  orbi12d  798  xorbi1d  1423  eueq2dc  2976  uneq1  3351  r19.45mv  3585  rexprg  3718  rextpg  3720  swopolem  4396  sowlin  4411  onsucelsucexmidlem1  4620  onsucelsucexmid  4622  ordsoexmid  4654  isosolem  5954  acexmidlema  5998  acexmidlemb  5999  acexmidlem2  6004  acexmidlemv  6005  freceq1  6544  exmidaclem  7401  exmidac  7402  elinp  7672  prloc  7689  suplocexprlemloc  7919  ltsosr  7962  suplocsrlemb  8004  axpre-ltwlin  8081  axpre-suploclemres  8099  axpre-suploc  8100  apreap  8745  apreim  8761  sup3exmid  9115  nn01to3  9824  ltxr  9983  fzpr  10285  elfzp12  10307  lcmval  12600  lcmass  12622  isprm6  12684  lringuplu  14175  domneq0  14251  znidom  14636  dedekindeulemloc  15308  dedekindeulemeu  15311  suplociccreex  15313  dedekindicclemloc  15317  dedekindicclemeu  15320  perfectlem2  15689