Theorem orbi1d 929

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

Syntax hints:   → wi 4   ↔ wb 209   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  orbi1  930  orbi12d  931  eueq2  3682  uneq1  4123  r19.45zv  4471  rexprgf  4663  rextpg  4667  swopolem  5577  ordsseleq  6388  ordtri3  6395  frxp2  8136  xpord2pred  8137  xpord2indlem  8139  frxp3  8143  xpord3pred  8144  infltoreq  9460  cantnflem1  9654  axgroth2  10806  axgroth3  10812  lelttric  11313  ltxr  13136  xmulneg1  13291  fzpr  13603  elfzp12  13627  caubnd  15406  lcmval  16646  lcmass  16668  isprm6  16769  vdwlem10  17046  irredmul  20507  lringuplu  20625  domneq0  20789  prmidl  21432  prmidlprop  21441  znfld  21675  opsrval  22162  logreclem  26889  perfectlem2  27356  nnm1n0s  28530  bdaypw2n0bndlem  28618  legov3  28829  lnhl  28846  colperpex  28969  lmif  29048  islmib  29050  friendshipgt3  30686  h1datom  31871  xrlelttric  33034  tlt3  33227  domnprodeq0  33536  ismxidl  33686  rprmdvds  33750  esumpcvgval  34409  sibfof  34671  satfvsuc  35748  satfv1  35750  satfvsucsuc  35752  satf0suc  35763  sat1el2xp  35766  fmlasuc0  35771  fmlafvel  35772  satfv1fvfmla1  35810  segcon2  36492  axtcond  36874  wl-ifpimpr  37995  poimirlem25  38179  cnambfre  38202  pridl  38571  ismaxidl  38574  ispridlc  38604  pridlc  38605  dmnnzd  38609  disjecxrncnvep  38947  4atlem3a  40256  pmapjoin  40511  lcfl3  42153  lcfl4N  42154  sticksstones22  42820  quadfac  42857  ordsssucb  43949  sbcoreleleqVD  45454  fourierdlem80  46787  euoreqb  47730  el1fzopredsuc  47947  perfectALTVlem2  48371  nnsum3primesle9  48443  clnbupgrel  48483  dfvopnbgr2  48502  lindslinindsimp2  49123