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  4459  elunsn  4637  rexprgf  4649  rextpg  4653  swopolem  5539  poleloe  6085  elsucg  6384  elsuc2g  6385  xpord2indlem  8086  brdifun  8661  brwdom  9464  isfin1a  10194  elgch  10524  suplem2pr  10955  axlttri  11195  mulcan1g  11781  elznn0  12494  elznn  12495  zindd  12584  rpneg  12930  dfle2  13052  fzm1  13514  fzosplitsni  13686  hashv01gt1  14259  zeo5  16274  bitsf1  16364  lcmval  16510  lcmneg  16521  lcmass  16532  isprm6  16632  infpn2  16832  irredmul  20356  lringuplu  20468  domneq0  20632  znfld  21506  quotval  26247  plydivlem4  26251  plydivex  26252  aalioulem2  26288  aalioulem5  26291  aalioulem6  26292  aaliou  26293  aaliou2  26295  aaliou2b  26296  elzs2  28343  elznns  28346  isinag  28836  axcontlem7  28969  hashecclwwlkn1  30078  eliccioo  32940  tlt2  32979  prmidl  33449  mxidlval  33470  rprmdvds  33528  sibfof  34425  ballotlemfc0  34578  ballotlemfcc  34579  satfvsucsuc  35481  satf0op  35493  fmlafvel  35501  isfmlasuc  35504  satfv1fvfmla1  35539  seglelin  36232  lineunray  36263  topdifinfeq  37467  wl-ifp4impr  37584  mblfinlem2  37771  pridl  38150  maxidlval  38152  ispridlc  38183  pridlc  38184  dmnnzd  38188  lcfl7N  41673  aomclem8  43218  fzuntgd  43615  orbi1r  44667  iccpartgtl  47588  iccpartleu  47590  clnbupgrel  47996  dfsclnbgr6  48020  lindslinindsimp2lem5  48624  lindslinindsimp2  48625  rrx2pnedifcoorneorr  48879