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  2937  uneq1  3310  r19.45mv  3544  rexprg  3674  rextpg  3676  swopolem  4340  sowlin  4355  onsucelsucexmidlem1  4564  onsucelsucexmid  4566  ordsoexmid  4598  isosolem  5871  acexmidlema  5913  acexmidlemb  5914  acexmidlem2  5919  acexmidlemv  5920  freceq1  6450  exmidaclem  7275  exmidac  7276  elinp  7541  prloc  7558  suplocexprlemloc  7788  ltsosr  7831  suplocsrlemb  7873  axpre-ltwlin  7950  axpre-suploclemres  7968  axpre-suploc  7969  apreap  8614  apreim  8630  sup3exmid  8984  nn01to3  9691  ltxr  9850  fzpr  10152  elfzp12  10174  lcmval  12231  lcmass  12253  isprm6  12315  lringuplu  13752  domneq0  13828  znidom  14213  dedekindeulemloc  14855  dedekindeulemeu  14858  suplociccreex  14860  dedekindicclemloc  14864  dedekindicclemeu  14867  perfectlem2  15236