Theorem orbi1d 786

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

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

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 704

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orbi1  787  orbi12d  788  xorbi1d  1376  eueq2dc  2903  uneq1  3274  r19.45mv  3507  rexprg  3633  rextpg  3635  swopolem  4288  sowlin  4303  onsucelsucexmidlem1  4510  onsucelsucexmid  4512  ordsoexmid  4544  isosolem  5800  acexmidlema  5841  acexmidlemb  5842  acexmidlem2  5847  acexmidlemv  5848  freceq1  6368  exmidaclem  7172  exmidac  7173  elinp  7423  prloc  7440  suplocexprlemloc  7670  ltsosr  7713  suplocsrlemb  7755  axpre-ltwlin  7832  axpre-suploclemres  7850  axpre-suploc  7851  apreap  8493  apreim  8509  sup3exmid  8860  nn01to3  9563  ltxr  9719  fzpr  10020  elfzp12  10042  lcmval  12004  lcmass  12026  isprm6  12088  dedekindeulemloc  13312  dedekindeulemeu  13315  suplociccreex  13317  dedekindicclemloc  13321  dedekindicclemeu  13324