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  3668  uneq1  4113  r19.45zv  4461  rexprgf  4652  rextpg  4656  swopolem  5542  ordsseleq  6346  ordtri3  6353  frxp2  8086  xpord2pred  8087  xpord2indlem  8089  frxp3  8093  xpord3pred  8094  infltoreq  9407  cantnflem1  9598  axgroth2  10736  axgroth3  10742  lelttric  11240  ltxr  13029  xmulneg1  13184  fzpr  13495  elfzp12  13519  caubnd  15282  lcmval  16519  lcmass  16541  isprm6  16641  vdwlem10  16918  irredmul  20365  lringuplu  20477  domneq0  20641  znfld  21515  opsrval  22001  logreclem  26728  perfectlem2  27197  nnm1n0s  28371  bdaypw2n0bndlem  28459  legov3  28670  lnhl  28687  colperpex  28805  lmif  28857  islmib  28859  friendshipgt3  30473  h1datom  31657  xrlelttric  32832  tlt3  33052  domnprodeq0  33358  prmidl  33521  ismxidl  33543  rprmdvds  33600  esumpcvgval  34235  sibfof  34497  satfvsuc  35555  satfv1  35557  satfvsucsuc  35559  satf0suc  35570  sat1el2xp  35573  fmlasuc0  35578  fmlafvel  35579  satfv1fvfmla1  35617  segcon2  36299  wl-ifpimpr  37671  poimirlem25  37846  cnambfre  37869  pridl  38238  ismaxidl  38241  ispridlc  38271  pridlc  38272  dmnnzd  38276  disjecxrncnvep  38598  4atlem3a  39857  pmapjoin  40112  lcfl3  41754  lcfl4N  41755  sticksstones22  42422  ordsssucb  43577  sbcoreleleqVD  45099  fourierdlem80  46430  euoreqb  47355  el1fzopredsuc  47571  perfectALTVlem2  47968  nnsum3primesle9  48040  clnbupgrel  48080  dfvopnbgr2  48099  lindslinindsimp2  48709