Theorem orbi1d 746

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

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orbi1  747  orbi12d  748  xorbi1d  1327  eueq2dc  2810  uneq1  3170  r19.45mv  3403  rexprg  3522  rextpg  3524  swopolem  4165  sowlin  4180  onsucelsucexmidlem1  4381  onsucelsucexmid  4383  ordsoexmid  4415  isosolem  5657  acexmidlema  5697  acexmidlemb  5698  acexmidlem2  5703  acexmidlemv  5704  freceq1  6219  elinp  7183  prloc  7200  ltsosr  7460  axpre-ltwlin  7568  apreap  8215  apreim  8231  sup3exmid  8573  nn01to3  9259  ltxr  9403  fzpr  9698  elfzp12  9720  lcmval  11537  lcmass  11559  isprm6  11618