Theorem orbi1d 796

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

Syntax hints:   → wi 4   ↔ wb 105   ∨ wo 713

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1  797  orbi12d  798  xorbi1d  1423  eueq2dc  2977  uneq1  3352  r19.45mv  3586  rexprg  3719  rextpg  3721  swopolem  4400  sowlin  4415  onsucelsucexmidlem1  4624  onsucelsucexmid  4626  ordsoexmid  4658  isosolem  5960  acexmidlema  6004  acexmidlemb  6005  acexmidlem2  6010  acexmidlemv  6011  freceq1  6553  exmidaclem  7413  exmidac  7414  elinp  7684  prloc  7701  suplocexprlemloc  7931  ltsosr  7974  suplocsrlemb  8016  axpre-ltwlin  8093  axpre-suploclemres  8111  axpre-suploc  8112  apreap  8757  apreim  8773  sup3exmid  9127  nn01to3  9841  ltxr  10000  fzpr  10302  elfzp12  10324  lcmval  12625  lcmass  12647  isprm6  12709  lringuplu  14200  domneq0  14276  znidom  14661  dedekindeulemloc  15333  dedekindeulemeu  15336  suplociccreex  15338  dedekindicclemloc  15342  dedekindicclemeu  15345  perfectlem2  15714