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  3718  uneq1  4170  r19.45zv  4508  rexprgf  4699  rextpg  4703  swopolem  5606  ordsseleq  6414  ordtri3  6421  frxp2  8167  xpord2pred  8168  xpord2indlem  8170  frxp3  8174  xpord3pred  8175  infltoreq  9539  cantnflem1  9726  axgroth2  10862  axgroth3  10868  lelttric  11365  ltxr  13154  xmulneg1  13307  fzpr  13615  elfzp12  13639  caubnd  15393  lcmval  16625  lcmass  16647  isprm6  16747  vdwlem10  17023  irredmul  20445  lringuplu  20560  domneq0  20724  znfld  21596  opsrval  22081  logreclem  26819  perfectlem2  27288  legov3  28620  lnhl  28637  colperpex  28755  lmif  28807  islmib  28809  friendshipgt3  30426  h1datom  31610  xrlelttric  32762  tlt3  32944  prmidl  33447  ismxidl  33469  rprmdvds  33526  esumpcvgval  34058  sibfof  34321  satfvsuc  35345  satfv1  35347  satfvsucsuc  35349  satf0suc  35360  sat1el2xp  35363  fmlasuc0  35368  fmlafvel  35369  satfv1fvfmla1  35407  segcon2  36086  wl-ifpimpr  37448  poimirlem25  37631  cnambfre  37654  pridl  38023  ismaxidl  38026  ispridlc  38056  pridlc  38057  dmnnzd  38061  disjecxrncnvep  38371  4atlem3a  39579  pmapjoin  39834  lcfl3  41476  lcfl4N  41477  sticksstones22  42149  ordsssucb  43324  sbcoreleleqVD  44856  fourierdlem80  46141  euoreqb  47058  el1fzopredsuc  47274  perfectALTVlem2  47646  nnsum3primesle9  47718  clnbupgrel  47758  dfvopnbgr2  47776  lindslinindsimp2  48308