Theorem orbi1d 915

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

Syntax hints:   → wi 4   ↔ wb 205   ∨ wo 845

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 206  df-or 846

This theorem is referenced by:  orbi1  916  orbi12d  917  eueq2  3671  uneq1  4121  r19.45zv  4465  rexprgf  4659  rextpg  4665  swopolem  5560  ordsseleq  6351  ordtri3  6358  frxp2  8081  xpord2pred  8082  xpord2indlem  8084  frxp3  8088  xpord3pred  8089  infltoreq  9447  cantnflem1  9634  axgroth2  10770  axgroth3  10776  lelttric  11271  ltxr  13045  xmulneg1  13198  fzpr  13506  elfzp12  13530  caubnd  15255  lcmval  16479  lcmass  16501  isprm6  16601  vdwlem10  16873  irredmul  20154  lringuplu  20224  domneq0  20804  znfld  21004  opsrval  21484  logreclem  26149  perfectlem2  26615  legov3  27603  lnhl  27620  colperpex  27738  lmif  27790  islmib  27792  friendshipgt3  29405  h1datom  30587  xrlelttric  31725  tlt3  31900  prmidl  32288  ismxidl  32307  esumpcvgval  32766  sibfof  33029  satfvsuc  34042  satfv1  34044  satfvsucsuc  34046  satf0suc  34057  sat1el2xp  34060  fmlasuc0  34065  fmlafvel  34066  satfv1fvfmla1  34104  segcon2  34766  wl-ifpimpr  36010  poimirlem25  36176  cnambfre  36199  pridl  36569  ismaxidl  36572  ispridlc  36602  pridlc  36603  dmnnzd  36607  disjecxrncnvep  36925  4atlem3a  38133  pmapjoin  38388  lcfl3  40030  lcfl4N  40031  sticksstones22  40649  ordsssucb  41728  sbcoreleleqVD  43263  fourierdlem80  44547  euoreqb  45461  el1fzopredsuc  45677  perfectALTVlem2  46034  nnsum3primesle9  46106  lindslinindsimp2  46664