Theorem orbi1d 798

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

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

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1  799  orbi12d  800  xorbi1d  1425  eueq2dc  2979  uneq1  3354  r19.45mv  3588  rexprg  3721  rextpg  3723  swopolem  4402  sowlin  4417  onsucelsucexmidlem1  4626  onsucelsucexmid  4628  ordsoexmid  4660  isosolem  5965  acexmidlema  6009  acexmidlemb  6010  acexmidlem2  6015  acexmidlemv  6016  freceq1  6558  exmidaclem  7423  exmidac  7424  elinp  7694  prloc  7711  suplocexprlemloc  7941  ltsosr  7984  suplocsrlemb  8026  axpre-ltwlin  8103  axpre-suploclemres  8121  axpre-suploc  8122  apreap  8767  apreim  8783  sup3exmid  9137  nn01to3  9851  ltxr  10010  fzpr  10312  elfzp12  10334  lcmval  12640  lcmass  12662  isprm6  12724  lringuplu  14216  domneq0  14292  znidom  14677  dedekindeulemloc  15349  dedekindeulemeu  15352  suplociccreex  15354  dedekindicclemloc  15358  dedekindicclemeu  15361  perfectlem2  15730