Theorem orbi2d 915

Description: Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-1993.)

Hypothesis

Ref	Expression
bid.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
orbi2d	⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒)))

Proof of Theorem orbi2d

Step	Hyp	Ref	Expression
1		bid.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	imbi2d 340	. 2 ⊢ (𝜑 → ((¬ 𝜃 → 𝜓) ↔ (¬ 𝜃 → 𝜒)))
3		df-or 848	. 2 ⊢ ((𝜃 ∨ 𝜓) ↔ (¬ 𝜃 → 𝜓))
4		df-or 848	. 2 ⊢ ((𝜃 ∨ 𝜒) ↔ (¬ 𝜃 → 𝜒))
5	2, 3, 4	3bitr4g 314	1 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒)))

Syntax hints:  ¬ wn 3   → 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:  orbi1d  916  orbi12d  918  eueq2  3684  sbc2or  3765  r19.44zv  4470  elunsn  4650  rexprgf  4662  rextpg  4666  swopolem  5559  poleloe  6107  elsucg  6405  elsuc2g  6406  xpord2indlem  8129  brdifun  8704  brwdom  9527  isfin1a  10252  elgch  10582  suplem2pr  11013  axlttri  11252  mulcan1g  11838  elznn0  12551  elznn  12552  zindd  12642  rpneg  12992  dfle2  13114  fzm1  13575  fzosplitsni  13746  hashv01gt1  14317  zeo5  16333  bitsf1  16423  lcmval  16569  lcmneg  16580  lcmass  16591  isprm6  16691  infpn2  16891  irredmul  20345  lringuplu  20460  domneq0  20624  znfld  21477  quotval  26207  plydivlem4  26211  plydivex  26212  aalioulem2  26248  aalioulem5  26251  aalioulem6  26252  aaliou  26253  aaliou2  26255  aaliou2b  26256  elzs2  28294  elznns  28297  isinag  28772  axcontlem7  28904  hashecclwwlkn1  30013  eliccioo  32858  tlt2  32902  prmidl  33418  mxidlval  33439  rprmdvds  33497  sibfof  34338  ballotlemfc0  34491  ballotlemfcc  34492  satfvsucsuc  35359  satf0op  35371  fmlafvel  35379  isfmlasuc  35382  satfv1fvfmla1  35417  seglelin  36111  lineunray  36142  topdifinfeq  37345  wl-ifp4impr  37462  mblfinlem2  37659  pridl  38038  maxidlval  38040  ispridlc  38071  pridlc  38072  dmnnzd  38076  lcfl7N  41502  aomclem8  43057  fzuntgd  43454  orbi1r  44507  iccpartgtl  47431  iccpartleu  47433  clnbupgrel  47839  dfsclnbgr6  47862  lindslinindsimp2lem5  48455  lindslinindsimp2  48456  rrx2pnedifcoorneorr  48710