Theorem orbi1d 916

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

Syntax hints:   → wi 4   ↔ wb 205   ∨ wo 846

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 206  df-or 847

This theorem is referenced by:  orbi1  917  orbi12d  918  eueq2  3707  uneq1  4157  r19.45zv  4503  rexprgf  4698  rextpg  4704  swopolem  5599  ordsseleq  6394  ordtri3  6401  frxp2  8130  xpord2pred  8131  xpord2indlem  8133  frxp3  8137  xpord3pred  8138  infltoreq  9497  cantnflem1  9684  axgroth2  10820  axgroth3  10826  lelttric  11321  ltxr  13095  xmulneg1  13248  fzpr  13556  elfzp12  13580  caubnd  15305  lcmval  16529  lcmass  16551  isprm6  16651  vdwlem10  16923  irredmul  20243  lringuplu  20314  domneq0  20913  znfld  21116  opsrval  21601  logreclem  26267  perfectlem2  26733  legov3  27880  lnhl  27897  colperpex  28015  lmif  28067  islmib  28069  friendshipgt3  29682  h1datom  30866  xrlelttric  31996  tlt3  32171  prmidl  32589  ismxidl  32609  esumpcvgval  33107  sibfof  33370  satfvsuc  34383  satfv1  34385  satfvsucsuc  34387  satf0suc  34398  sat1el2xp  34401  fmlasuc0  34406  fmlafvel  34407  satfv1fvfmla1  34445  segcon2  35108  wl-ifpimpr  36395  poimirlem25  36561  cnambfre  36584  pridl  36953  ismaxidl  36956  ispridlc  36986  pridlc  36987  dmnnzd  36991  disjecxrncnvep  37308  4atlem3a  38516  pmapjoin  38771  lcfl3  40413  lcfl4N  40414  sticksstones22  41032  ordsssucb  42133  sbcoreleleqVD  43668  fourierdlem80  44950  euoreqb  45865  el1fzopredsuc  46081  perfectALTVlem2  46438  nnsum3primesle9  46510  lindslinindsimp2  47192