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  3665  uneq1  4110  r19.45zv  4458  rexprgf  4649  rextpg  4653  swopolem  5539  ordsseleq  6343  ordtri3  6350  frxp2  8083  xpord2pred  8084  xpord2indlem  8086  frxp3  8090  xpord3pred  8091  infltoreq  9399  cantnflem1  9590  axgroth2  10727  axgroth3  10733  lelttric  11231  ltxr  13020  xmulneg1  13175  fzpr  13486  elfzp12  13510  caubnd  15273  lcmval  16510  lcmass  16532  isprm6  16632  vdwlem10  16909  irredmul  20356  lringuplu  20468  domneq0  20632  znfld  21506  opsrval  21992  logreclem  26719  perfectlem2  27188  nnm1n0s  28320  legov3  28596  lnhl  28613  colperpex  28731  lmif  28783  islmib  28785  friendshipgt3  30399  h1datom  31583  xrlelttric  32760  tlt3  32980  domnprodeq0  33286  prmidl  33449  ismxidl  33471  rprmdvds  33528  esumpcvgval  34163  sibfof  34425  satfvsuc  35477  satfv1  35479  satfvsucsuc  35481  satf0suc  35492  sat1el2xp  35495  fmlasuc0  35500  fmlafvel  35501  satfv1fvfmla1  35539  segcon2  36221  wl-ifpimpr  37583  poimirlem25  37758  cnambfre  37781  pridl  38150  ismaxidl  38153  ispridlc  38183  pridlc  38184  dmnnzd  38188  disjecxrncnvep  38510  4atlem3a  39769  pmapjoin  40024  lcfl3  41666  lcfl4N  41667  sticksstones22  42334  ordsssucb  43492  sbcoreleleqVD  45015  fourierdlem80  46346  euoreqb  47271  el1fzopredsuc  47487  perfectALTVlem2  47884  nnsum3primesle9  47956  clnbupgrel  47996  dfvopnbgr2  48015  lindslinindsimp2  48625