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  3548  vtocl3gaOLD  3550  axdc4uz  13949  wrdl3s3  14928  relexpindlem  15029  sqrtval  15203  sqreu  15327  coprmprod  16631  mreexexd  17609  iscatd2  17642  lmodprop2d  20830  neiptopnei  23019  hausnei  23215  isreg2  23264  regr1lem2  23627  ustval  24090  ustuqtop4  24132  axtgupdim2  28398  axtgeucl  28399  iscgra  28736  brbtwn  28826  ax5seg  28865  axlowdim  28888  axeuclidlem  28889  wlkonprop  29586  upgr2wlk  29596  upgrf1istrl  29631  elwspths2spth  29897  clwlkclwwlk  29931  clwwlknonel  30024  upgr4cycl4dv4e  30114  extwwlkfab  30281  nvi  30543  br8d  32538  xlt2addrd  32682  isslmd  33155  slmdlema  33156  constrllcllem  33742  constrcbvlem  33745  tgoldbachgt  34654  axtgupdim2ALTV  34659  br8  35743  br6  35744  br4  35745  fvtransport  36020  brcolinear2  36046  colineardim1  36049  fscgr  36068  idinside  36072  brsegle  36096  poimirlem28  37642  caures  37754  iscringd  37992  oposlem  39175  cdleme18d  40289  jm2.27  42997  ichexmpl2  47471  ichnreuop  47473  9gbo  47775  11gbo  47776