Theorem 3anbi1d 1442

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 1439	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜏) ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))

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

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 1088

This theorem is referenced by:  vtocl3gafOLD  3561  vtocl3gaOLD  3563  axdc4uz  14000  wrdl3s3  14979  relexpindlem  15080  sqrtval  15254  sqreu  15377  coprmprod  16678  mreexexd  17658  iscatd2  17691  lmodprop2d  20879  neiptopnei  23068  hausnei  23264  isreg2  23313  regr1lem2  23676  ustval  24139  ustuqtop4  24181  axtgupdim2  28396  axtgeucl  28397  iscgra  28734  brbtwn  28824  ax5seg  28863  axlowdim  28886  axeuclidlem  28887  wlkonprop  29584  upgr2wlk  29594  upgrf1istrl  29629  elwspths2spth  29895  clwlkclwwlk  29929  clwwlknonel  30022  upgr4cycl4dv4e  30112  extwwlkfab  30279  nvi  30541  br8d  32536  xlt2addrd  32682  isslmd  33145  slmdlema  33146  constrllcllem  33732  constrcbvlem  33735  tgoldbachgt  34641  axtgupdim2ALTV  34646  br8  35719  br6  35720  br4  35721  fvtransport  35996  brcolinear2  36022  colineardim1  36025  fscgr  36044  idinside  36048  brsegle  36072  poimirlem28  37618  caures  37730  iscringd  37968  oposlem  39146  cdleme18d  40260  jm2.27  42979  ichexmpl2  47432  ichnreuop  47434  9gbo  47736  11gbo  47737