Theorem orbi1d 929

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

Syntax hints:   → wi 4   ↔ wb 209   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  orbi1  930  orbi12d  931  eueq2  3673  uneq1  4115  r19.45zv  4469  rexprgf  4661  rextpg  4665  swopolem  5579  ordsseleq  6390  ordtri3  6397  frxp2  8136  xpord2pred  8137  xpord2indlem  8139  frxp3  8143  xpord3pred  8144  infltoreq  9460  cantnflem1  9654  axgroth2  10805  axgroth3  10811  lelttric  11312  ltxr  13135  xmulneg1  13290  fzpr  13603  elfzp12  13627  caubnd  15406  lcmval  16645  lcmass  16667  isprm6  16768  vdwlem10  17045  irredmul  20507  lringuplu  20643  domneq0  20807  prmidl  21465  prmidlprop  21476  znfld  21710  opsrval  22197  logreclem  26927  perfectlem2  27394  nnm1n0s  28568  bdaypw2n0bndlem  28656  legov3  28867  lnhl  28887  colperpex  29014  lmif  29094  islmib  29096  friendshipgt3  30749  h1datom  31934  xrlelttric  33097  tlt3  33290  domnprodeq0  33599  ismxidl  33745  rprmdvds  33809  esumpcvgval  34468  sibfof  34730  satfvsuc  35853  satfv1  35855  satfvsucsuc  35857  satf0suc  35868  sat1el2xp  35871  fmlasuc0  35876  fmlafvel  35877  satfv1fvfmla1  35915  segcon2  36597  axtcond  36989  wl-ifpimpr  38112  poimirlem25  38296  cnambfre  38319  pridl  38688  ismaxidl  38691  ispridlc  38721  pridlc  38722  dmnnzd  38726  disjecxrncnvep  39062  4atlem3a  40371  pmapjoin  40626  lcfl3  42268  lcfl4N  42269  sticksstones22  42935  quadfac  42972  ordsssucb  44062  sbcoreleleqVD  45567  fourierdlem80  46900  euoreqb  47846  el1fzopredsuc  48063  perfectALTVlem2  48487  nnsum3primesle9  48559  clnbupgrel  48599  dfvopnbgr2  48618  idomnzd  49111  lindslinindsimp2  49243