Theorem 3anbi1d 1443

Description: Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)

Hypothesis

Ref	Expression
3anbi1d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
3anbi1d	⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜏) ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))

Proof of Theorem 3anbi1d

Step	Hyp	Ref	Expression
1		3anbi1d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		biidd 262	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃))
3	1, 2	3anbi12d 1440	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜏) ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1087

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-an 396  df-3an 1089

This theorem is referenced by:  vtocl3gafOLD  3526  vtocl3gaOLD  3528  axdc4uz  13940  wrdl3s3  14918  relexpindlem  15019  sqrtval  15193  sqreu  15317  coprmprod  16624  mreexexd  17608  iscatd2  17641  lmodprop2d  20913  neiptopnei  23110  hausnei  23306  isreg2  23355  regr1lem2  23718  ustval  24181  ustuqtop4  24222  bdayfinbndcbv  28475  bdayfinbndlem1  28476  bdayfinbndlem2  28477  bdayfinbnd  28478  axtgupdim2  28556  axtgeucl  28557  iscgra  28894  brbtwn  28985  ax5seg  29024  axlowdim  29047  axeuclidlem  29048  wlkonprop  29743  upgr2wlk  29753  upgrf1istrl  29788  elwspths2spth  30056  clwlkclwwlk  30090  clwwlknonel  30183  upgr4cycl4dv4e  30273  extwwlkfab  30440  nvi  30703  br8d  32699  xlt2addrd  32850  isslmd  33281  slmdlema  33282  constrllcllem  33915  constrcbvlem  33918  tgoldbachgt  34826  axtgupdim2ALTV  34831  trssfir1om  35274  trssfir1omregs  35299  br8  35957  br6  35958  br4  35959  fvtransport  36233  brcolinear2  36259  colineardim1  36262  fscgr  36281  idinside  36285  brsegle  36309  poimirlem28  37986  caures  38098  iscringd  38336  oposlem  39645  cdleme18d  40758  jm2.27  43457  ichexmpl2  47945  ichnreuop  47947  9gbo  48265  11gbo  48266