Theorem orbi1d 930

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  orbi1  931  orbi12d  932  eueq2  3671  uneq1  4163  r19.45zv  4467  rexprgf  4657  rextpg  4661  swopolem  5576  ordsseleq  6418  ordtri3  6425  frxp2  8198  xpord2pred  8199  xpord2indlem  8201  frxp3  8205  xpord3pred  8206  infltoreq  9533  cantnflem1  9727  axgroth2  10949  axgroth3  10955  lelttric  11456  ltxr  13284  xmulneg1  13439  fzpr  13753  elfzp12  13777  caubnd  15570  lcmval  16811  lcmass  16833  isprm6  16934  vdwlem10  17212  irredmul  20710  lringuplu  20847  domneq0  21011  prmidl  21672  prmidlprop  21683  znfld  21921  opsrval  22410  logreclem  27147  perfectlem2  27614  nnm1n0s  28818  bdaypw2n0bndlem  28906  legov3  29118  lnhl  29138  colperpex  29266  lmif  29347  islmib  29349  friendshipgt3  31056  h1datom  32241  xrlelttric  33440  tlt3  33627  domnprodeq0  33939  isedom  33953  ismxidl  34091  rprmdvds  34155  esumpcvgval  34821  sibfof  35083  satfvsuc  36334  satfv1  36336  satfvsucsuc  36338  satf0suc  36349  sat1el2xp  36352  fmlasuc0  36357  fmlafvel  36358  satfv1fvfmla1  36396  segcon2  37085  axtcond  37481  wl-ifpimpr  38657  poimirlem25  38831  cnambfre  38854  varprop  38910  negprop  38911  impprop  38912  dfprop2  38914  pridl  39237  ismaxidl  39240  ispridlc  39270  pridlc  39271  dmnnzd  39275  disjecxrncnvep  39611  4atlem3a  40920  pmapjoin  41175  lcfl3  42817  lcfl4N  42818  sticksstones22  43484  quadfac  43521  ordsssucb  44598  sbcoreleleqVD  46101  fourierdlem80  47469  euoreqb  48453  el1fzopredsuc  48669  perfectALTVlem2  49093  nnsum3primesle9  49165  clnbupgrel  49205  dfvopnbgr2  49224  idomnzd  49774  lindslinindsimp2  49906