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  3667  uneq1  4160  r19.45zv  4463  rexprgf  4652  rextpg  4656  swopolem  5568  ordsseleq  6392  ordtri3  6399  frxp2  8164  xpord2pred  8165  xpord2indlem  8167  frxp3  8171  xpord3pred  8172  infltoreq  9500  cantnflem1  9694  axgroth2  10914  axgroth3  10920  lelttric  11421  ltxr  13248  xmulneg1  13403  fzpr  13717  elfzp12  13741  caubnd  15532  lcmval  16773  lcmass  16795  isprm6  16896  vdwlem10  17174  irredmul  20665  lringuplu  20802  domneq0  20966  prmidl  21627  prmidlprop  21638  znfld  21872  opsrval  22361  logreclem  27096  perfectlem2  27563  nnm1n0s  28767  bdaypw2n0bndlem  28855  legov3  29067  lnhl  29087  colperpex  29215  lmif  29296  islmib  29298  friendshipgt3  31005  h1datom  32190  xrlelttric  33391  tlt3  33578  domnprodeq0  33887  ismxidl  34034  rprmdvds  34098  esumpcvgval  34757  sibfof  35019  satfvsuc  36213  satfv1  36215  satfvsucsuc  36217  satf0suc  36228  sat1el2xp  36231  fmlasuc0  36236  fmlafvel  36237  satfv1fvfmla1  36275  segcon2  36963  axtcond  37359  wl-ifpimpr  38483  poimirlem25  38657  cnambfre  38680  varprop  38736  negprop  38737  impprop  38738  dfprop2  38740  pridl  39065  ismaxidl  39068  ispridlc  39098  pridlc  39099  dmnnzd  39103  disjecxrncnvep  39439  4atlem3a  40748  pmapjoin  41003  lcfl3  42645  lcfl4N  42646  sticksstones22  43312  quadfac  43349  ordsssucb  44431  sbcoreleleqVD  45935  fourierdlem80  47290  euoreqb  48273  el1fzopredsuc  48490  perfectALTVlem2  48914  nnsum3primesle9  48986  clnbupgrel  49026  dfvopnbgr2  49045  idomnzd  49537  lindslinindsimp2  49669