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  1392  eueq2dc  2925  uneq1  3297  r19.45mv  3531  rexprg  3659  rextpg  3661  swopolem  4323  sowlin  4338  onsucelsucexmidlem1  4545  onsucelsucexmid  4547  ordsoexmid  4579  isosolem  5845  acexmidlema  5886  acexmidlemb  5887  acexmidlem2  5892  acexmidlemv  5893  freceq1  6416  exmidaclem  7236  exmidac  7237  elinp  7502  prloc  7519  suplocexprlemloc  7749  ltsosr  7792  suplocsrlemb  7834  axpre-ltwlin  7911  axpre-suploclemres  7929  axpre-suploc  7930  apreap  8573  apreim  8589  sup3exmid  8943  nn01to3  9646  ltxr  9804  fzpr  10106  elfzp12  10128  lcmval  12094  lcmass  12116  isprm6  12178  lringuplu  13540  dedekindeulemloc  14549  dedekindeulemeu  14552  suplociccreex  14554  dedekindicclemloc  14558  dedekindicclemeu  14561