Theorem orbi1d 916

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

Syntax hints:   → wi 4   ↔ wb 206   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  orbi1  917  orbi12d  918  eueq2  3664  uneq1  4106  r19.45zv  4448  rexprgf  4643  rextpg  4647  swopolem  5529  ordsseleq  6330  ordtri3  6337  frxp2  8069  xpord2pred  8070  xpord2indlem  8072  frxp3  8076  xpord3pred  8077  infltoreq  9383  cantnflem1  9574  axgroth2  10711  axgroth3  10717  lelttric  11215  ltxr  13009  xmulneg1  13163  fzpr  13474  elfzp12  13498  caubnd  15261  lcmval  16498  lcmass  16520  isprm6  16620  vdwlem10  16897  irredmul  20342  lringuplu  20454  domneq0  20618  znfld  21492  opsrval  21976  logreclem  26694  perfectlem2  27163  nnm1n0s  28295  legov3  28571  lnhl  28588  colperpex  28706  lmif  28758  islmib  28760  friendshipgt3  30370  h1datom  31554  xrlelttric  32727  tlt3  32943  prmidl  33397  ismxidl  33419  rprmdvds  33476  esumpcvgval  34083  sibfof  34345  satfvsuc  35397  satfv1  35399  satfvsucsuc  35401  satf0suc  35412  sat1el2xp  35415  fmlasuc0  35420  fmlafvel  35421  satfv1fvfmla1  35459  segcon2  36139  wl-ifpimpr  37500  poimirlem25  37685  cnambfre  37708  pridl  38077  ismaxidl  38080  ispridlc  38110  pridlc  38111  dmnnzd  38115  disjecxrncnvep  38422  4atlem3a  39636  pmapjoin  39891  lcfl3  41533  lcfl4N  41534  sticksstones22  42201  ordsssucb  43368  sbcoreleleqVD  44891  fourierdlem80  46224  euoreqb  47140  el1fzopredsuc  47356  perfectALTVlem2  47753  nnsum3primesle9  47825  clnbupgrel  47865  dfvopnbgr2  47884  lindslinindsimp2  48495