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  3668  sbc2or  3748  r19.44zv  4465  elunsn  4644  rexprgf  4656  rextpg  4660  swopolem  5569  poleloe  6125  elsucg  6432  elsuc2g  6433  xpord2indlem  8157  brdifun  8741  brwdom  9554  isfin1a  10363  elgch  10700  suplem2pr  11131  axlttri  11374  mulcan1g  11962  elznn0  12701  elznn  12702  zindd  12793  rpneg  13147  dfle2  13269  fzm1  13734  fzosplitsni  13907  hashv01gt1  14482  zeo5  16519  bitsf1  16609  lcmval  16760  lcmneg  16771  lcmass  16782  isprm6  16883  infpn2  17084  irredmul  20652  lringuplu  20789  domneq0  20953  prmidl  21614  prmidlprop  21625  znfld  21859  quotval  26606  plydivlem4  26610  plydivex  26611  aalioulem2  26653  aalioulem5  26656  aalioulem6  26657  aaliou  26658  aaliou2  26660  aaliou2b  26661  elzs2  28778  elznns  28781  elplng  29251  plngcplem  29256  isinag  29350  brprlng  29409  axcontlem7  29541  hashecclwwlkn1  30661  eliccioo  33490  tlt2  33523  mxidlval  33979  rprmdvds  34044  sibfof  34965  ballotlemfc0  35118  ballotlemfcc  35119  satfvsucsuc  36109  satf0op  36121  fmlafvel  36129  isfmlasuc  36132  satfv1fvfmla1  36167  seglelin  36861  lineunray  36892  topdifinfeq  38253  wl-ifp4impr  38370  mblfinlem2  38556  varprop  38622  negprop  38623  impprop  38624  dfprop2  38626  pridl  38951  maxidlval  38953  ispridlc  38984  pridlc  38985  dmnnzd  38989  lcfl7N  42538  aomclem8  44047  fzuntgd  44443  orbi1r  45478  iccpartgtl  48477  iccpartleu  48479  nprmmul3  48580  clnbupgrel  48901  dfsclnbgr6  48925  idomnzd  49412  lindslinindsimp2lem5  49543  lindslinindsimp2  49544  rrx2pnedifcoorneorr  49798