Theorem orbi2d 928

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

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∨ wo 860

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 210  df-or 861

This theorem is referenced by:  orbi1d  929  orbi12d  931  eueq2  3682  sbc2or  3762  r19.44zv  4472  elunsn  4651  rexprgf  4663  rextpg  4667  swopolem  5577  poleloe  6129  elsucg  6428  elsuc2g  6429  xpord2indlem  8139  brdifun  8721  brwdom  9525  isfin1a  10272  elgch  10603  suplem2pr  11034  axlttri  11277  mulcan1g  11863  elznn0  12602  elznn  12603  zindd  12693  rpneg  13046  dfle2  13168  fzm1  13631  fzosplitsni  13804  hashv01gt1  14377  zeo5  16410  bitsf1  16500  lcmval  16646  lcmneg  16657  lcmass  16668  isprm6  16769  infpn2  16969  irredmul  20507  lringuplu  20625  domneq0  20789  prmidl  21432  prmidlprop  21441  znfld  21675  quotval  26418  plydivlem4  26422  plydivex  26423  aalioulem2  26459  aalioulem5  26462  aalioulem6  26463  aaliou  26464  aaliou2  26466  aaliou2b  26467  elzs2  28554  elznns  28557  elplng  29016  plngcplem  29021  isinag  29106  brprlng  29139  axcontlem7  29257  hashecclwwlkn1  30365  eliccioo  33187  tlt2  33226  mxidlval  33685  rprmdvds  33750  sibfof  34671  ballotlemfc0  34824  ballotlemfcc  34825  satfvsucsuc  35752  satf0op  35764  fmlafvel  35772  isfmlasuc  35775  satfv1fvfmla1  35810  seglelin  36503  lineunray  36534  topdifinfeq  37879  wl-ifp4impr  37996  mblfinlem2  38192  pridl  38571  maxidlval  38573  ispridlc  38604  pridlc  38605  dmnnzd  38609  lcfl7N  42160  aomclem8  43673  fzuntgd  44069  orbi1r  45104  iccpartgtl  48057  iccpartleu  48059  nprmmul3  48160  clnbupgrel  48481  dfsclnbgr6  48505  lindslinindsimp2lem5  49120  lindslinindsimp2  49121  rrx2pnedifcoorneorr  49375