Theorem orbi1d 927

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

Syntax hints:   → wi 4   ↔ wb 208   ∨ wo 858

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 209  df-or 859

This theorem is referenced by:  orbi1  928  orbi12d  929  eueq2  3671  uneq1  4112  r19.45zv  4459  rexprgf  4651  rextpg  4655  swopolem  5561  ordsseleq  6370  ordtri3  6377  frxp2  8118  xpord2pred  8119  xpord2indlem  8121  frxp3  8125  xpord3pred  8126  infltoreq  9444  cantnflem1  9638  axgroth2  10777  axgroth3  10783  lelttric  11284  ltxr  13111  xmulneg1  13266  fzpr  13578  elfzp12  13602  caubnd  15377  lcmval  16617  lcmass  16639  isprm6  16740  vdwlem10  17017  irredmul  20465  lringuplu  20581  domneq0  20745  znfld  21600  opsrval  22087  logreclem  26815  perfectlem2  27282  nnm1n0s  28456  bdaypw2n0bndlem  28544  legov3  28755  lnhl  28772  colperpex  28890  lmif  28942  islmib  28944  friendshipgt3  30557  h1datom  31742  xrlelttric  32915  tlt3  33109  domnprodeq0  33421  prmidl  33587  prmidlprop  33596  ismxidl  33611  rprmdvds  33676  esumpcvgval  34336  sibfof  34598  satfvsuc  35672  satfv1  35674  satfvsucsuc  35676  satf0suc  35687  sat1el2xp  35690  fmlasuc0  35695  fmlafvel  35696  satfv1fvfmla1  35734  segcon2  36416  axtcond  36799  wl-ifpimpr  37921  poimirlem25  38105  cnambfre  38128  pridl  38497  ismaxidl  38500  ispridlc  38530  pridlc  38531  dmnnzd  38535  disjecxrncnvep  38873  4atlem3a  40182  pmapjoin  40437  lcfl3  42079  lcfl4N  42080  sticksstones22  42746  ordsssucb  43873  sbcoreleleqVD  45395  fourierdlem80  46721  euoreqb  47664  el1fzopredsuc  47881  perfectALTVlem2  48305  nnsum3primesle9  48377  clnbupgrel  48417  dfvopnbgr2  48436  lindslinindsimp2  49046