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  3311  r19.45mv  3545  rexprg  3675  rextpg  3677  swopolem  4341  sowlin  4356  onsucelsucexmidlem1  4565  onsucelsucexmid  4567  ordsoexmid  4599  isosolem  5874  acexmidlema  5916  acexmidlemb  5917  acexmidlem2  5922  acexmidlemv  5923  freceq1  6459  exmidaclem  7293  exmidac  7294  elinp  7560  prloc  7577  suplocexprlemloc  7807  ltsosr  7850  suplocsrlemb  7892  axpre-ltwlin  7969  axpre-suploclemres  7987  axpre-suploc  7988  apreap  8633  apreim  8649  sup3exmid  9003  nn01to3  9710  ltxr  9869  fzpr  10171  elfzp12  10193  lcmval  12258  lcmass  12280  isprm6  12342  lringuplu  13830  domneq0  13906  znidom  14291  dedekindeulemloc  14963  dedekindeulemeu  14966  suplociccreex  14968  dedekindicclemloc  14972  dedekindicclemeu  14975  perfectlem2  15344