Theorem orbi1d 803

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   ∨ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  orbi1  804  orbi12d  805  xorbi1d  1430  eueq2dc  2999  uneq1  3376  r19.45mv  3621  rexprg  3761  rextpg  3763  swopolem  4450  sowlin  4465  onsucelsucexmidlem1  4675  onsucelsucexmid  4677  ordsoexmid  4709  isosolem  6030  acexmidlema  6076  acexmidlemb  6077  acexmidlem2  6082  acexmidlemv  6083  freceq1  6663  exmidaclem  7565  exmidac  7566  papcotr  7614  elinp  7842  prloc  7859  suplocexprlemloc  8089  ltsosr  8132  suplocsrlemb  8174  axpre-ltwlin  8251  axpre-suploclemres  8269  axpre-suploc  8270  apreap  8918  apreim  8934  sup3exmid  9290  nn01to3  10027  ltxr  10188  fzpr  10495  elfzp12  10517  lcmval  12860  lcmass  12882  isprm6  12945  ballotfilemfc0  13284  ballotfilemfcc  13285  lringuplu  14587  domneq0  14665  znidom  15076  dedekindeulemloc  15811  dedekindeulemeu  15814  suplociccreex  15816  dedekindicclemloc  15820  dedekindicclemeu  15823  perfectlem2  16261