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  2954  uneq1  3329  r19.45mv  3563  rexprg  3696  rextpg  3698  swopolem  4371  sowlin  4386  onsucelsucexmidlem1  4595  onsucelsucexmid  4597  ordsoexmid  4629  isosolem  5918  acexmidlema  5960  acexmidlemb  5961  acexmidlem2  5966  acexmidlemv  5967  freceq1  6503  exmidaclem  7353  exmidac  7354  elinp  7624  prloc  7641  suplocexprlemloc  7871  ltsosr  7914  suplocsrlemb  7956  axpre-ltwlin  8033  axpre-suploclemres  8051  axpre-suploc  8052  apreap  8697  apreim  8713  sup3exmid  9067  nn01to3  9775  ltxr  9934  fzpr  10236  elfzp12  10258  lcmval  12546  lcmass  12568  isprm6  12630  lringuplu  14119  domneq0  14195  znidom  14580  dedekindeulemloc  15252  dedekindeulemeu  15255  suplociccreex  15257  dedekindicclemloc  15261  dedekindicclemeu  15264  perfectlem2  15633