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  3698  uneq1  4141  r19.45zv  4483  rexprgf  4676  rextpg  4680  swopolem  5576  ordsseleq  6386  ordtri3  6393  frxp2  8148  xpord2pred  8149  xpord2indlem  8151  frxp3  8155  xpord3pred  8156  infltoreq  9521  cantnflem1  9708  axgroth2  10844  axgroth3  10850  lelttric  11347  ltxr  13136  xmulneg1  13290  fzpr  13601  elfzp12  13625  caubnd  15382  lcmval  16616  lcmass  16638  isprm6  16738  vdwlem10  17015  irredmul  20394  lringuplu  20509  domneq0  20673  znfld  21526  opsrval  22009  logreclem  26729  perfectlem2  27198  nnm1n0s  28321  legov3  28582  lnhl  28599  colperpex  28717  lmif  28769  islmib  28771  friendshipgt3  30384  h1datom  31568  xrlelttric  32734  tlt3  32955  prmidl  33460  ismxidl  33482  rprmdvds  33539  esumpcvgval  34114  sibfof  34377  satfvsuc  35388  satfv1  35390  satfvsucsuc  35392  satf0suc  35403  sat1el2xp  35406  fmlasuc0  35411  fmlafvel  35412  satfv1fvfmla1  35450  segcon2  36128  wl-ifpimpr  37489  poimirlem25  37674  cnambfre  37697  pridl  38066  ismaxidl  38069  ispridlc  38099  pridlc  38100  dmnnzd  38104  disjecxrncnvep  38413  4atlem3a  39621  pmapjoin  39876  lcfl3  41518  lcfl4N  41519  sticksstones22  42186  ordsssucb  43334  sbcoreleleqVD  44858  fourierdlem80  46195  euoreqb  47118  el1fzopredsuc  47334  perfectALTVlem2  47716  nnsum3primesle9  47788  clnbupgrel  47828  dfvopnbgr2  47846  lindslinindsimp2  48419