Theorem orbi1d 945

Description: Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-1993.)

Hypothesis

Ref	Expression
bid.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
orbi1d	⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃)))

Proof of Theorem orbi1d

Step	Hyp	Ref	Expression
1		bid.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	orbi2d 944	. 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒)))
3		orcom 901	. 2 ⊢ ((𝜓 ∨ 𝜃) ↔ (𝜃 ∨ 𝜓))
4		orcom 901	. 2 ⊢ ((𝜒 ∨ 𝜃) ↔ (𝜃 ∨ 𝜒))
5	2, 3, 4	3bitr4g 306	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 198   ∨ wo 878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 199  df-or 879

This theorem is referenced by:  orbi1  946  orbi12d  947  eueq2  3605  uneq1  3987  r19.45zv  4290  rexprg  4454  rextpg  4456  swopolem  5272  ordsseleq  5992  ordtri3  5999  infltoreq  8677  cantnflem1  8863  axgroth2  9962  axgroth3  9968  lelttric  10463  ltxr  12235  xmulneg1  12387  fzpr  12689  elfzp12  12713  caubnd  14475  lcmval  15678  lcmass  15700  isprm6  15797  vdwlem10  16065  irredmul  19063  domneq0  19658  opsrval  19835  znfld  20268  logreclem  24902  perfectlem2  25368  legov3  25910  lnhl  25927  colperpex  26042  lmif  26094  islmib  26096  friendshipgt3  27802  h1datom  28985  xrlelttric  30053  tlt3  30199  esumpcvgval  30674  sibfof  30936  segcon2  32740  poimirlem25  33971  cnambfre  33994  pridl  34371  ismaxidl  34374  ispridlc  34404  pridlc  34405  dmnnzd  34409  4atlem3a  35665  pmapjoin  35920  lcfl3  37562  lcfl4N  37563  sbcoreleleqVD  39906  fourierdlem80  41190  el1fzopredsuc  42216  perfectALTVlem2  42454  nnsum3primesle9  42505  lindslinindsimp2  43092