Theorem orbi1d 738

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

Syntax hints:   → wi 4   ↔ wb 103   ∨ wo 662

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  orbi1  739  orbi12d  740  xorbi1d  1313  eueq2dc  2776  uneq1  3131  r19.45mv  3356  rexprg  3468  rextpg  3470  swopolem  4096  sowlin  4111  onsucelsucexmidlem1  4307  onsucelsucexmid  4309  ordsoexmid  4341  isosolem  5542  acexmidlema  5582  acexmidlemb  5583  acexmidlem2  5588  acexmidlemv  5589  freceq1  6089  elinp  6936  prloc  6953  ltsosr  7213  axpre-ltwlin  7321  apreap  7964  apreim  7980  nn01to3  8997  ltxr  9141  fzpr  9384  elfzp12  9406  lcmval  10825  lcmass  10847  isprm6  10906