Theorem 3anbi1d 1443

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

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

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 1089

This theorem is referenced by:  vtocl3gafOLD  3539  vtocl3gaOLD  3541  axdc4uz  13919  wrdl3s3  14897  relexpindlem  14998  sqrtval  15172  sqreu  15296  coprmprod  16600  mreexexd  17583  iscatd2  17616  lmodprop2d  20887  neiptopnei  23088  hausnei  23284  isreg2  23333  regr1lem2  23696  ustval  24159  ustuqtop4  24200  bdayfinbndcbv  28474  bdayfinbndlem1  28475  bdayfinbndlem2  28476  bdayfinbnd  28477  axtgupdim2  28555  axtgeucl  28556  iscgra  28893  brbtwn  28984  ax5seg  29023  axlowdim  29046  axeuclidlem  29047  wlkonprop  29742  upgr2wlk  29752  upgrf1istrl  29787  elwspths2spth  30055  clwlkclwwlk  30089  clwwlknonel  30182  upgr4cycl4dv4e  30272  extwwlkfab  30439  nvi  30702  br8d  32698  xlt2addrd  32850  isslmd  33296  slmdlema  33297  constrllcllem  33930  constrcbvlem  33933  tgoldbachgt  34841  axtgupdim2ALTV  34846  trssfir1om  35289  trssfir1omregs  35314  br8  35972  br6  35973  br4  35974  fvtransport  36248  brcolinear2  36274  colineardim1  36277  fscgr  36296  idinside  36300  brsegle  36324  poimirlem28  37899  caures  38011  iscringd  38249  oposlem  39558  cdleme18d  40671  jm2.27  43365  ichexmpl2  47830  ichnreuop  47832  9gbo  48134  11gbo  48135