Theorem orbi2d 922

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 342	. 2 ⊢ (𝜑 → ((¬ 𝜃 → 𝜓) ↔ (¬ 𝜃 → 𝜒)))
3		df-or 855	. 2 ⊢ ((𝜃 ∨ 𝜓) ↔ (¬ 𝜃 → 𝜓))
4		df-or 855	. 2 ⊢ ((𝜃 ∨ 𝜒) ↔ (¬ 𝜃 → 𝜒))
5	2, 3, 4	3bitr4g 316	1 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∨ wo 854

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 209  df-or 855

This theorem is referenced by:  orbi1d  923  orbi12d  925  eueq2  3652  sbc2or  3733  r19.44zv  4439  elunsn  4617  rexprgf  4629  rextpg  4633  swopolem  5538  poleloe  6087  elsucg  6383  elsuc2g  6384  xpord2indlem  8089  brdifun  8668  brwdom  9476  isfin1a  10210  elgch  10541  suplem2pr  10972  axlttri  11213  mulcan1g  11799  elznn0  12534  elznn  12535  zindd  12625  rpneg  12971  dfle2  13093  fzm1  13556  fzosplitsni  13729  hashv01gt1  14302  zeo5  16320  bitsf1  16410  lcmval  16556  lcmneg  16567  lcmass  16578  isprm6  16679  infpn2  16879  irredmul  20403  lringuplu  20519  domneq0  20683  znfld  21538  quotval  26279  plydivlem4  26283  plydivex  26284  aalioulem2  26320  aalioulem5  26323  aalioulem6  26324  aaliou  26325  aaliou2  26327  aaliou2b  26328  elzs2  28411  elznns  28414  isinag  28926  axcontlem7  29059  hashecclwwlkn1  30167  eliccioo  33011  tlt2  33050  prmidl  33525  mxidlval  33546  rprmdvds  33612  sibfof  34534  ballotlemfc0  34687  ballotlemfcc  34688  satfvsucsuc  35606  satf0op  35618  fmlafvel  35626  isfmlasuc  35629  satfv1fvfmla1  35664  seglelin  36357  lineunray  36388  topdifinfeq  37725  wl-ifp4impr  37842  mblfinlem2  38038  pridl  38417  maxidlval  38419  ispridlc  38450  pridlc  38451  dmnnzd  38455  lcfl7N  42006  aomclem8  43519  fzuntgd  43915  orbi1r  44967  iccpartgtl  47913  iccpartleu  47915  nprmmul3  48016  clnbupgrel  48337  dfsclnbgr6  48361  lindslinindsimp2lem5  48965  lindslinindsimp2  48966  rrx2pnedifcoorneorr  49220