Theorem orbi1d 791

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

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

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1  792  orbi12d  793  xorbi1d  1381  eueq2dc  2911  uneq1  3283  r19.45mv  3517  rexprg  3645  rextpg  3647  swopolem  4306  sowlin  4321  onsucelsucexmidlem1  4528  onsucelsucexmid  4530  ordsoexmid  4562  isosolem  5825  acexmidlema  5866  acexmidlemb  5867  acexmidlem2  5872  acexmidlemv  5873  freceq1  6393  exmidaclem  7207  exmidac  7208  elinp  7473  prloc  7490  suplocexprlemloc  7720  ltsosr  7763  suplocsrlemb  7805  axpre-ltwlin  7882  axpre-suploclemres  7900  axpre-suploc  7901  apreap  8544  apreim  8560  sup3exmid  8914  nn01to3  9617  ltxr  9775  fzpr  10077  elfzp12  10099  lcmval  12063  lcmass  12085  isprm6  12147  lringuplu  13337  dedekindeulemloc  14100  dedekindeulemeu  14103  suplociccreex  14105  dedekindicclemloc  14109  dedekindicclemeu  14112