Theorem 3anbi1d 1468

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 265	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃))
3	1, 2	3anbi12d 1465	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜏) ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  axdc4uz  14120  wrdl3s3  15108  relexpindlem  15209  sqrtval  15397  sqreu  15521  coprmprod  16829  mreexexd  17815  iscatd2  17848  lmodprop2d  21192  neiptopnei  23443  hausnei  23639  isreg2  23688  regr1lem2  24052  ustval  24515  ustuqtop4  24556  bdayfinbndcbv  28845  bdayfinbndlem1  28846  bdayfinbndlem2  28847  bdayfinbnd  28848  axtgupdim2  28926  axtgeucl  28927  iscgra  29309  brbtwn  29470  ax5seg  29509  axlowdim  29532  axeuclidlem  29533  wlkonprop  30230  upgr2wlk  30240  upgrf1istrl  30279  elwspths2spth  30552  clwlkclwwlk  30586  clwwlknonel  30679  upgr4cycl4dv4e  30779  extwwlkfab  30946  nvi  31209  br8d  33195  xlt2addrd  33344  isslmd  33756  slmdlema  33757  constrllcllem  34377  constrcbvlem  34380  tgoldbachgt  35285  axtgupdim2ALTV  35290  trssfir1om  35726  trssfir1omregs  35787  br8  36500  br6  36501  br4  36502  fvtransport  36777  brcolinear2  36803  colineardim1  36806  fscgr  36825  idinside  36829  brsegle  36853  poimirlem28  38546  caures  38674  iscringd  38912  oposlem  40219  cdleme18d  41332  jm2.27  43994  ichexmpl2  48521  ichnreuop  48523  9gbo  48841  11gbo  48842