Theorem orbi1d 799

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

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

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1  800  orbi12d  801  xorbi1d  1426  eueq2dc  2992  uneq1  3368  r19.45mv  3605  rexprg  3743  rextpg  3745  swopolem  4428  sowlin  4443  onsucelsucexmidlem1  4652  onsucelsucexmid  4654  ordsoexmid  4686  isosolem  5999  acexmidlema  6043  acexmidlemb  6044  acexmidlem2  6049  acexmidlemv  6050  freceq1  6625  exmidaclem  7517  exmidac  7518  papcotr  7564  elinp  7791  prloc  7808  suplocexprlemloc  8038  ltsosr  8081  suplocsrlemb  8123  axpre-ltwlin  8200  axpre-suploclemres  8218  axpre-suploc  8219  apreap  8863  apreim  8879  sup3exmid  9233  nn01to3  9952  ltxr  10111  fzpr  10415  elfzp12  10437  lcmval  12764  lcmass  12786  isprm6  12848  ballotfilemfc0  13153  ballotfilemfcc  13154  lringuplu  14358  domneq0  14435  znidom  14822  dedekindeulemloc  15501  dedekindeulemeu  15504  suplociccreex  15506  dedekindicclemloc  15510  dedekindicclemeu  15513  perfectlem2  15885