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  7564  exmidac  7565  papcotr  7613  elinp  7841  prloc  7858  suplocexprlemloc  8088  ltsosr  8131  suplocsrlemb  8173  axpre-ltwlin  8250  axpre-suploclemres  8268  axpre-suploc  8269  apreap  8917  apreim  8933  sup3exmid  9289  nn01to3  10026  ltxr  10187  fzpr  10494  elfzp12  10516  lcmval  12857  lcmass  12879  isprm6  12942  ballotfilemfc0  13281  ballotfilemfcc  13282  lringuplu  14552  domneq0  14630  znidom  15041  dedekindeulemloc  15769  dedekindeulemeu  15772  suplociccreex  15774  dedekindicclemloc  15778  dedekindicclemeu  15781  perfectlem2  16198