Theorem orbi1d 914

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

Syntax hints:   → wi 4   ↔ wb 209   ∨ wo 844

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 210  df-or 845

This theorem is referenced by:  orbi1  915  orbi12d  916  eueq2  3649  uneq1  4083  r19.45zv  4406  rexprgf  4591  rextpg  4595  swopolem  5447  ordsseleq  6188  ordtri3  6195  infltoreq  8950  cantnflem1  9136  axgroth2  10236  axgroth3  10242  lelttric  10736  ltxr  12498  xmulneg1  12650  fzpr  12957  elfzp12  12981  caubnd  14710  lcmval  15926  lcmass  15948  isprm6  16048  vdwlem10  16316  irredmul  19455  domneq0  20063  znfld  20252  opsrval  20714  logreclem  25348  perfectlem2  25814  legov3  26392  lnhl  26409  colperpex  26527  lmif  26579  islmib  26581  friendshipgt3  28183  h1datom  29365  xrlelttric  30502  tlt3  30678  prmidl  31023  ismxidl  31042  esumpcvgval  31447  sibfof  31708  satfvsuc  32721  satfv1  32723  satfvsucsuc  32725  satf0suc  32736  sat1el2xp  32739  fmlasuc0  32744  fmlafvel  32745  satfv1fvfmla1  32783  segcon2  33679  wl-ifpimpr  34883  poimirlem25  35082  cnambfre  35105  pridl  35475  ismaxidl  35478  ispridlc  35508  pridlc  35509  dmnnzd  35513  4atlem3a  36893  pmapjoin  37148  lcfl3  38790  lcfl4N  38791  sbcoreleleqVD  41565  fourierdlem80  42828  euoreqb  43665  el1fzopredsuc  43882  perfectALTVlem2  44240  nnsum3primesle9  44312  lindslinindsimp2  44872