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  3537  vtocl3gaOLD  3539  axdc4uz  13891  wrdl3s3  14869  relexpindlem  14970  sqrtval  15144  sqreu  15268  coprmprod  16572  mreexexd  17554  iscatd2  17587  lmodprop2d  20827  neiptopnei  23017  hausnei  23213  isreg2  23262  regr1lem2  23625  ustval  24088  ustuqtop4  24130  axtgupdim2  28416  axtgeucl  28417  iscgra  28754  brbtwn  28844  ax5seg  28883  axlowdim  28906  axeuclidlem  28907  wlkonprop  29602  upgr2wlk  29612  upgrf1istrl  29647  elwspths2spth  29912  clwlkclwwlk  29946  clwwlknonel  30039  upgr4cycl4dv4e  30129  extwwlkfab  30296  nvi  30558  br8d  32555  xlt2addrd  32702  isslmd  33144  slmdlema  33145  constrllcllem  33719  constrcbvlem  33722  tgoldbachgt  34631  axtgupdim2ALTV  34636  br8  35729  br6  35730  br4  35731  fvtransport  36006  brcolinear2  36032  colineardim1  36035  fscgr  36054  idinside  36058  brsegle  36082  poimirlem28  37628  caures  37740  iscringd  37978  oposlem  39161  cdleme18d  40274  jm2.27  42981  ichexmpl2  47454  ichnreuop  47456  9gbo  47758  11gbo  47759