Theorem 3anbi1d 1461

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1098

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 209  df-an 400  df-3an 1100

This theorem is referenced by:  axdc4uz  13997  wrdl3s3  14975  relexpindlem  15076  sqrtval  15264  sqreu  15388  coprmprod  16695  mreexexd  17680  iscatd2  17713  lmodprop2d  20988  neiptopnei  23189  hausnei  23385  isreg2  23434  regr1lem2  23797  ustval  24260  ustuqtop4  24301  bdayfinbndcbv  28556  bdayfinbndlem1  28557  bdayfinbndlem2  28558  bdayfinbnd  28559  axtgupdim2  28637  axtgeucl  28638  iscgra  29000  brbtwn  29097  ax5seg  29136  axlowdim  29159  axeuclidlem  29160  wlkonprop  29854  upgr2wlk  29864  upgrf1istrl  29899  elwspths2spth  30167  clwlkclwwlk  30201  clwwlknonel  30294  upgr4cycl4dv4e  30384  extwwlkfab  30551  nvi  30814  br8d  32807  xlt2addrd  32958  isslmd  33379  slmdlema  33380  constrllcllem  34046  constrcbvlem  34049  tgoldbachgt  34954  axtgupdim2ALTV  34959  trssfir1om  35404  trssfir1omregs  35429  br8  36103  br6  36104  br4  36105  fvtransport  36379  brcolinear2  36405  colineardim1  36408  fscgr  36427  idinside  36431  brsegle  36455  poimirlem28  38144  caures  38256  iscringd  38494  oposlem  39803  cdleme18d  40916  jm2.27  43582  ichexmpl2  48073  ichnreuop  48075  9gbo  48393  11gbo  48394