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  3675  uneq1  4115  r19.45zv  4471  rexprgf  4663  rextpg  4667  swopolem  5581  ordsseleq  6394  ordtri3  6401  frxp2  8142  xpord2pred  8143  xpord2indlem  8145  frxp3  8149  xpord3pred  8150  infltoreq  9467  cantnflem1  9661  axgroth2  10821  axgroth3  10827  lelttric  11328  ltxr  13152  xmulneg1  13307  fzpr  13620  elfzp12  13644  caubnd  15430  lcmval  16668  lcmass  16690  isprm6  16791  vdwlem10  17068  irredmul  20537  lringuplu  20673  domneq0  20837  prmidl  21495  prmidlprop  21506  znfld  21740  opsrval  22227  logreclem  26958  perfectlem2  27425  nnm1n0s  28599  bdaypw2n0bndlem  28687  legov3  28898  lnhl  28918  colperpex  29045  lmif  29125  islmib  29127  friendshipgt3  30796  h1datom  31981  xrlelttric  33143  tlt3  33330  domnprodeq0  33639  ismxidl  33785  rprmdvds  33849  esumpcvgval  34508  sibfof  34771  satfvsuc  35866  satfv1  35868  satfvsucsuc  35870  satf0suc  35881  sat1el2xp  35884  fmlasuc0  35889  fmlafvel  35890  satfv1fvfmla1  35928  segcon2  36610  axtcond  37022  wl-ifpimpr  38145  poimirlem25  38329  cnambfre  38352  pridl  38721  ismaxidl  38724  ispridlc  38754  pridlc  38755  dmnnzd  38759  disjecxrncnvep  39095  4atlem3a  40404  pmapjoin  40659  lcfl3  42301  lcfl4N  42302  sticksstones22  42968  quadfac  43005  ordsssucb  44095  sbcoreleleqVD  45600  fourierdlem80  46933  euoreqb  47879  el1fzopredsuc  48096  perfectALTVlem2  48520  nnsum3primesle9  48592  clnbupgrel  48632  dfvopnbgr2  48651  idomnzd  49144  lindslinindsimp2  49276