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  4351  sowlin  4366  onsucelsucexmidlem1  4575  onsucelsucexmid  4577  ordsoexmid  4609  isosolem  5892  acexmidlema  5934  acexmidlemb  5935  acexmidlem2  5940  acexmidlemv  5941  freceq1  6477  exmidaclem  7319  exmidac  7320  elinp  7586  prloc  7603  suplocexprlemloc  7833  ltsosr  7876  suplocsrlemb  7918  axpre-ltwlin  7995  axpre-suploclemres  8013  axpre-suploc  8014  apreap  8659  apreim  8675  sup3exmid  9029  nn01to3  9737  ltxr  9896  fzpr  10198  elfzp12  10220  lcmval  12327  lcmass  12349  isprm6  12411  lringuplu  13900  domneq0  13976  znidom  14361  dedekindeulemloc  15033  dedekindeulemeu  15036  suplociccreex  15038  dedekindicclemloc  15042  dedekindicclemeu  15045  perfectlem2  15414