Theorem orbi1d 917

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

Syntax hints:   → wi 4   ↔ wb 206   ∨ wo 848

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 849

This theorem is referenced by:  orbi1  918  orbi12d  919  eueq2  3656  uneq1  4101  r19.45zv  4448  rexprgf  4639  rextpg  4643  swopolem  5549  ordsseleq  6352  ordtri3  6359  frxp2  8094  xpord2pred  8095  xpord2indlem  8097  frxp3  8101  xpord3pred  8102  infltoreq  9417  cantnflem1  9610  axgroth2  10748  axgroth3  10754  lelttric  11253  ltxr  13066  xmulneg1  13221  fzpr  13533  elfzp12  13557  caubnd  15321  lcmval  16561  lcmass  16583  isprm6  16684  vdwlem10  16961  irredmul  20409  lringuplu  20521  domneq0  20685  znfld  21540  opsrval  22024  logreclem  26726  perfectlem2  27193  nnm1n0s  28367  bdaypw2n0bndlem  28455  legov3  28666  lnhl  28683  colperpex  28801  lmif  28853  islmib  28855  friendshipgt3  30468  h1datom  31653  xrlelttric  32825  tlt3  33030  domnprodeq0  33337  prmidl  33500  ismxidl  33522  rprmdvds  33579  esumpcvgval  34222  sibfof  34484  satfvsuc  35543  satfv1  35545  satfvsucsuc  35547  satf0suc  35558  sat1el2xp  35561  fmlasuc0  35566  fmlafvel  35567  satfv1fvfmla1  35605  segcon2  36287  axtcond  36660  wl-ifpimpr  37782  poimirlem25  37966  cnambfre  37989  pridl  38358  ismaxidl  38361  ispridlc  38391  pridlc  38392  dmnnzd  38396  disjecxrncnvep  38734  4atlem3a  40043  pmapjoin  40298  lcfl3  41940  lcfl4N  41941  sticksstones22  42607  ordsssucb  43763  sbcoreleleqVD  45285  fourierdlem80  46614  euoreqb  47557  el1fzopredsuc  47774  perfectALTVlem2  48198  nnsum3primesle9  48270  clnbupgrel  48310  dfvopnbgr2  48329  lindslinindsimp2  48939