Theorem orbi2d 929

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  orbi1d  930  orbi12d  932  eueq2  3667  sbc2or  3747  r19.44zv  4464  elunsn  4640  rexprgf  4652  rextpg  4656  swopolem  5568  poleloe  6124  elsucg  6433  elsuc2g  6434  xpord2indlem  8167  brdifun  8752  brwdom  9565  isfin1a  10374  elgch  10711  suplem2pr  11142  axlttri  11385  mulcan1g  11973  elznn0  12712  elznn  12713  zindd  12804  rpneg  13158  dfle2  13280  fzm1  13745  fzosplitsni  13918  hashv01gt1  14493  zeo5  16532  bitsf1  16622  lcmval  16773  lcmneg  16784  lcmass  16795  isprm6  16896  infpn2  17097  irredmul  20665  lringuplu  20802  domneq0  20966  prmidl  21627  prmidlprop  21638  znfld  21872  quotval  26619  plydivlem4  26623  plydivex  26624  aalioulem2  26666  aalioulem5  26669  aalioulem6  26670  aaliou  26671  aaliou2  26673  aaliou2b  26674  elzs2  28791  elznns  28794  elplng  29264  plngcplem  29269  isinag  29363  brprlng  29422  axcontlem7  29554  hashecclwwlkn1  30674  eliccioo  33544  tlt2  33577  mxidlval  34033  rprmdvds  34098  sibfof  35019  ballotlemfc0  35172  ballotlemfcc  35173  onf1oracwevd  35972  satfvsucsuc  36217  satf0op  36229  fmlafvel  36237  isfmlasuc  36240  satfv1fvfmla1  36275  seglelin  36974  lineunray  37005  topdifinfeq  38367  wl-ifp4impr  38484  mblfinlem2  38670  varprop  38736  negprop  38737  impprop  38738  dfprop2  38740  pridl  39065  maxidlval  39067  ispridlc  39098  pridlc  39099  dmnnzd  39103  lcfl7N  42652  aomclem8  44157  fzuntgd  44553  orbi1r  45587  iccpartgtl  48602  iccpartleu  48604  nprmmul3  48705  clnbupgrel  49026  dfsclnbgr6  49050  idomnzd  49537  lindslinindsimp2lem5  49668  lindslinindsimp2  49669  rrx2pnedifcoorneorr  49924