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  4395  sowlin  4410  onsucelsucexmidlem1  4619  onsucelsucexmid  4621  ordsoexmid  4653  isosolem  5947  acexmidlema  5991  acexmidlemb  5992  acexmidlem2  5997  acexmidlemv  5998  freceq1  6536  exmidaclem  7386  exmidac  7387  elinp  7657  prloc  7674  suplocexprlemloc  7904  ltsosr  7947  suplocsrlemb  7989  axpre-ltwlin  8066  axpre-suploclemres  8084  axpre-suploc  8085  apreap  8730  apreim  8746  sup3exmid  9100  nn01to3  9808  ltxr  9967  fzpr  10269  elfzp12  10291  lcmval  12580  lcmass  12602  isprm6  12664  lringuplu  14154  domneq0  14230  znidom  14615  dedekindeulemloc  15287  dedekindeulemeu  15290  suplociccreex  15292  dedekindicclemloc  15296  dedekindicclemeu  15299  perfectlem2  15668