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  3670  uneq1  4115  r19.45zv  4463  rexprgf  4654  rextpg  4658  swopolem  5550  ordsseleq  6354  ordtri3  6361  frxp2  8096  xpord2pred  8097  xpord2indlem  8099  frxp3  8103  xpord3pred  8104  infltoreq  9419  cantnflem1  9610  axgroth2  10748  axgroth3  10754  lelttric  11252  ltxr  13041  xmulneg1  13196  fzpr  13507  elfzp12  13531  caubnd  15294  lcmval  16531  lcmass  16553  isprm6  16653  vdwlem10  16930  irredmul  20377  lringuplu  20489  domneq0  20653  znfld  21527  opsrval  22013  logreclem  26740  perfectlem2  27209  nnm1n0s  28383  bdaypw2n0bndlem  28471  legov3  28682  lnhl  28699  colperpex  28817  lmif  28869  islmib  28871  friendshipgt3  30485  h1datom  31670  xrlelttric  32843  tlt3  33063  domnprodeq0  33370  prmidl  33533  ismxidl  33555  rprmdvds  33612  esumpcvgval  34256  sibfof  34518  satfvsuc  35577  satfv1  35579  satfvsucsuc  35581  satf0suc  35592  sat1el2xp  35595  fmlasuc0  35600  fmlafvel  35601  satfv1fvfmla1  35639  segcon2  36321  wl-ifpimpr  37721  poimirlem25  37896  cnambfre  37919  pridl  38288  ismaxidl  38291  ispridlc  38321  pridlc  38322  dmnnzd  38326  disjecxrncnvep  38664  4atlem3a  39973  pmapjoin  40228  lcfl3  41870  lcfl4N  41871  sticksstones22  42538  ordsssucb  43692  sbcoreleleqVD  45214  fourierdlem80  46544  euoreqb  47469  el1fzopredsuc  47685  perfectALTVlem2  48082  nnsum3primesle9  48154  clnbupgrel  48194  dfvopnbgr2  48213  lindslinindsimp2  48823