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  3551  vtocl3gaOLD  3553  axdc4uz  13956  wrdl3s3  14935  relexpindlem  15036  sqrtval  15210  sqreu  15334  coprmprod  16638  mreexexd  17616  iscatd2  17649  lmodprop2d  20837  neiptopnei  23026  hausnei  23222  isreg2  23271  regr1lem2  23634  ustval  24097  ustuqtop4  24139  axtgupdim2  28405  axtgeucl  28406  iscgra  28743  brbtwn  28833  ax5seg  28872  axlowdim  28895  axeuclidlem  28896  wlkonprop  29593  upgr2wlk  29603  upgrf1istrl  29638  elwspths2spth  29904  clwlkclwwlk  29938  clwwlknonel  30031  upgr4cycl4dv4e  30121  extwwlkfab  30288  nvi  30550  br8d  32545  xlt2addrd  32689  isslmd  33162  slmdlema  33163  constrllcllem  33749  constrcbvlem  33752  tgoldbachgt  34661  axtgupdim2ALTV  34666  br8  35750  br6  35751  br4  35752  fvtransport  36027  brcolinear2  36053  colineardim1  36056  fscgr  36075  idinside  36079  brsegle  36103  poimirlem28  37649  caures  37761  iscringd  37999  oposlem  39182  cdleme18d  40296  jm2.27  43004  ichexmpl2  47475  ichnreuop  47477  9gbo  47779  11gbo  47780