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  3672  uneq1  4114  r19.45zv  4456  rexprgf  4649  rextpg  4653  swopolem  5541  ordsseleq  6340  ordtri3  6347  frxp2  8084  xpord2pred  8085  xpord2indlem  8087  frxp3  8091  xpord3pred  8092  infltoreq  9413  cantnflem1  9604  axgroth2  10738  axgroth3  10744  lelttric  11242  ltxr  13036  xmulneg1  13190  fzpr  13501  elfzp12  13525  caubnd  15285  lcmval  16522  lcmass  16544  isprm6  16644  vdwlem10  16921  irredmul  20333  lringuplu  20448  domneq0  20612  znfld  21486  opsrval  21970  logreclem  26689  perfectlem2  27158  nnm1n0s  28288  legov3  28562  lnhl  28579  colperpex  28697  lmif  28749  islmib  28751  friendshipgt3  30361  h1datom  31545  xrlelttric  32714  tlt3  32931  prmidl  33396  ismxidl  33418  rprmdvds  33475  esumpcvgval  34064  sibfof  34327  satfvsuc  35353  satfv1  35355  satfvsucsuc  35357  satf0suc  35368  sat1el2xp  35371  fmlasuc0  35376  fmlafvel  35377  satfv1fvfmla1  35415  segcon2  36098  wl-ifpimpr  37459  poimirlem25  37644  cnambfre  37667  pridl  38036  ismaxidl  38039  ispridlc  38069  pridlc  38070  dmnnzd  38074  disjecxrncnvep  38381  4atlem3a  39596  pmapjoin  39851  lcfl3  41493  lcfl4N  41494  sticksstones22  42161  ordsssucb  43328  sbcoreleleqVD  44852  fourierdlem80  46187  euoreqb  47113  el1fzopredsuc  47329  perfectALTVlem2  47726  nnsum3primesle9  47798  clnbupgrel  47838  dfvopnbgr2  47857  lindslinindsimp2  48468