Theorem orbi2d 914

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∨ wo 846

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 847

This theorem is referenced by:  orbi1d  915  orbi12d  917  eueq2  3732  sbc2or  3813  r19.44zv  4527  rexprgf  4718  rextpg  4724  swopolem  5618  poleloe  6163  elsucg  6463  elsuc2g  6464  xpord2indlem  8188  brdifun  8793  brwdom  9636  isfin1a  10361  elgch  10691  suplem2pr  11122  axlttri  11361  mulcan1g  11943  elznn0  12654  elznn  12655  zindd  12744  rpneg  13089  dfle2  13209  fzm1  13664  fzosplitsni  13828  hashv01gt1  14394  zeo5  16404  bitsf1  16492  lcmval  16639  lcmneg  16650  lcmass  16661  isprm6  16761  infpn2  16960  irredmul  20455  lringuplu  20570  domneq0  20730  znfld  21602  quotval  26352  plydivlem4  26356  plydivex  26357  aalioulem2  26393  aalioulem5  26396  aalioulem6  26397  aaliou  26398  aaliou2  26400  aaliou2b  26401  elzs2  28403  elznns  28406  isinag  28864  axcontlem7  29003  hashecclwwlkn1  30109  elunsn  32541  eliccioo  32895  tlt2  32942  prmidl  33433  mxidlval  33454  rprmdvds  33512  sibfof  34305  ballotlemfc0  34457  ballotlemfcc  34458  satfvsucsuc  35333  satf0op  35345  fmlafvel  35353  isfmlasuc  35356  satfv1fvfmla1  35391  seglelin  36080  lineunray  36111  topdifinfeq  37316  wl-ifp4impr  37433  mblfinlem2  37618  pridl  37997  maxidlval  37999  ispridlc  38030  pridlc  38031  dmnnzd  38035  lcfl7N  41458  aomclem8  43018  fzuntgd  43420  orbi1r  44481  iccpartgtl  47300  iccpartleu  47302  clnbupgrel  47707  dfsclnbgr6  47730  lindslinindsimp2lem5  48191  lindslinindsimp2  48192  rrx2pnedifcoorneorr  48451