Theorem orbi1d 798

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

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

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1  799  orbi12d  800  xorbi1d  1425  eueq2dc  2979  uneq1  3354  r19.45mv  3588  rexprg  3721  rextpg  3723  swopolem  4402  sowlin  4417  onsucelsucexmidlem1  4626  onsucelsucexmid  4628  ordsoexmid  4660  isosolem  5964  acexmidlema  6008  acexmidlemb  6009  acexmidlem2  6014  acexmidlemv  6015  freceq1  6557  exmidaclem  7422  exmidac  7423  elinp  7693  prloc  7710  suplocexprlemloc  7940  ltsosr  7983  suplocsrlemb  8025  axpre-ltwlin  8102  axpre-suploclemres  8120  axpre-suploc  8121  apreap  8766  apreim  8782  sup3exmid  9136  nn01to3  9850  ltxr  10009  fzpr  10311  elfzp12  10333  lcmval  12634  lcmass  12656  isprm6  12718  lringuplu  14209  domneq0  14285  znidom  14670  dedekindeulemloc  15342  dedekindeulemeu  15345  suplociccreex  15347  dedekindicclemloc  15351  dedekindicclemeu  15354  perfectlem2  15723