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  3545  vtocl3gaOLD  3547  axdc4uz  13925  wrdl3s3  14904  relexpindlem  15005  sqrtval  15179  sqreu  15303  coprmprod  16607  mreexexd  17585  iscatd2  17618  lmodprop2d  20806  neiptopnei  22995  hausnei  23191  isreg2  23240  regr1lem2  23603  ustval  24066  ustuqtop4  24108  axtgupdim2  28374  axtgeucl  28375  iscgra  28712  brbtwn  28802  ax5seg  28841  axlowdim  28864  axeuclidlem  28865  wlkonprop  29560  upgr2wlk  29570  upgrf1istrl  29605  elwspths2spth  29870  clwlkclwwlk  29904  clwwlknonel  29997  upgr4cycl4dv4e  30087  extwwlkfab  30254  nvi  30516  br8d  32511  xlt2addrd  32655  isslmd  33128  slmdlema  33129  constrllcllem  33715  constrcbvlem  33718  tgoldbachgt  34627  axtgupdim2ALTV  34632  br8  35716  br6  35717  br4  35718  fvtransport  35993  brcolinear2  36019  colineardim1  36022  fscgr  36041  idinside  36045  brsegle  36069  poimirlem28  37615  caures  37727  iscringd  37965  oposlem  39148  cdleme18d  40262  jm2.27  42970  ichexmpl2  47444  ichnreuop  47446  9gbo  47748  11gbo  47749