Theorem orbi1d 780

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

Syntax hints:   → wi 4   ↔ wb 104   ∨ wo 697

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orbi1  781  orbi12d  782  xorbi1d  1359  eueq2dc  2857  uneq1  3223  r19.45mv  3456  rexprg  3575  rextpg  3577  swopolem  4227  sowlin  4242  onsucelsucexmidlem1  4443  onsucelsucexmid  4445  ordsoexmid  4477  isosolem  5725  acexmidlema  5765  acexmidlemb  5766  acexmidlem2  5771  acexmidlemv  5772  freceq1  6289  exmidaclem  7064  exmidac  7065  elinp  7282  prloc  7299  suplocexprlemloc  7529  ltsosr  7572  suplocsrlemb  7614  axpre-ltwlin  7691  axpre-suploclemres  7709  axpre-suploc  7710  apreap  8349  apreim  8365  sup3exmid  8715  nn01to3  9409  ltxr  9562  fzpr  9857  elfzp12  9879  lcmval  11744  lcmass  11766  isprm6  11825  dedekindeulemloc  12766  dedekindeulemeu  12769  suplociccreex  12771  dedekindicclemloc  12775  dedekindicclemeu  12778