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  3665  sbc2or  3746  r19.44zv  4453  elunsn  4635  rexprgf  4647  rextpg  4651  swopolem  5537  poleloe  6082  elsucg  6381  elsuc2g  6382  xpord2indlem  8083  brdifun  8658  brwdom  9460  isfin1a  10190  elgch  10520  suplem2pr  10951  axlttri  11191  mulcan1g  11777  elznn0  12490  elznn  12491  zindd  12580  rpneg  12926  dfle2  13048  fzm1  13509  fzosplitsni  13681  hashv01gt1  14254  zeo5  16269  bitsf1  16359  lcmval  16505  lcmneg  16516  lcmass  16527  isprm6  16627  infpn2  16827  irredmul  20349  lringuplu  20461  domneq0  20625  znfld  21499  quotval  26228  plydivlem4  26232  plydivex  26233  aalioulem2  26269  aalioulem5  26272  aalioulem6  26273  aaliou  26274  aaliou2  26276  aaliou2b  26277  elzs2  28324  elznns  28327  isinag  28817  axcontlem7  28950  hashecclwwlkn1  30059  eliccioo  32918  tlt2  32957  prmidl  33412  mxidlval  33433  rprmdvds  33491  sibfof  34374  ballotlemfc0  34527  ballotlemfcc  34528  satfvsucsuc  35430  satf0op  35442  fmlafvel  35450  isfmlasuc  35453  satfv1fvfmla1  35488  seglelin  36181  lineunray  36212  topdifinfeq  37415  wl-ifp4impr  37532  mblfinlem2  37718  pridl  38097  maxidlval  38099  ispridlc  38130  pridlc  38131  dmnnzd  38135  lcfl7N  41620  aomclem8  43178  fzuntgd  43575  orbi1r  44627  iccpartgtl  47550  iccpartleu  47552  clnbupgrel  47958  dfsclnbgr6  47982  lindslinindsimp2lem5  48587  lindslinindsimp2  48588  rrx2pnedifcoorneorr  48842