Theorem orbi1d 915

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

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

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 846

This theorem is referenced by:  orbi1  916  orbi12d  917  eueq2  3699  uneq1  4149  r19.45zv  4493  rexprgf  4687  rextpg  4693  swopolem  5588  ordsseleq  6379  ordtri3  6386  frxp2  8109  xpord2pred  8110  xpord2indlem  8112  frxp3  8116  xpord3pred  8117  infltoreq  9476  cantnflem1  9663  axgroth2  10799  axgroth3  10805  lelttric  11300  ltxr  13074  xmulneg1  13227  fzpr  13535  elfzp12  13559  caubnd  15284  lcmval  16508  lcmass  16530  isprm6  16630  vdwlem10  16902  irredmul  20190  lringuplu  20261  domneq0  20844  znfld  21044  opsrval  21524  logreclem  26189  perfectlem2  26655  legov3  27709  lnhl  27726  colperpex  27844  lmif  27896  islmib  27898  friendshipgt3  29511  h1datom  30693  xrlelttric  31831  tlt3  32006  prmidl  32401  ismxidl  32421  esumpcvgval  32891  sibfof  33154  satfvsuc  34167  satfv1  34169  satfvsucsuc  34171  satf0suc  34182  sat1el2xp  34185  fmlasuc0  34190  fmlafvel  34191  satfv1fvfmla1  34229  segcon2  34891  wl-ifpimpr  36135  poimirlem25  36301  cnambfre  36324  pridl  36694  ismaxidl  36697  ispridlc  36727  pridlc  36728  dmnnzd  36732  disjecxrncnvep  37049  4atlem3a  38257  pmapjoin  38512  lcfl3  40154  lcfl4N  40155  sticksstones22  40773  ordsssucb  41842  sbcoreleleqVD  43377  fourierdlem80  44661  euoreqb  45575  el1fzopredsuc  45791  perfectALTVlem2  46148  nnsum3primesle9  46220  lindslinindsimp2  46778