Theorem orbi1d 705

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

Syntax hints:   → wi 4   ↔ wb 98   ∨ wo 629

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  orbi1  706  orbi12d  707  xorbi1d  1272  eueq2dc  2714  uneq1  3090  r19.45mv  3315  rexprg  3422  rextpg  3424  swopolem  4042  sowlin  4057  onsucelsucexmidlem1  4253  onsucelsucexmid  4255  ordsoexmid  4286  isosolem  5463  acexmidlema  5503  acexmidlemb  5504  acexmidlem2  5509  acexmidlemv  5510  freceq1  5979  elinp  6572  prloc  6589  ltsosr  6849  axpre-ltwlin  6957  apreap  7578  apreim  7594  nn01to3  8552  ltxr  8695  fzpr  8939  elfzp12  8961