Theorem 3anbi1d 1570

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

Syntax hints:   → wi 4   ↔ wb 198   ∧ w3a 1113

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 199  df-an 387  df-3an 1115

This theorem is referenced by:  vtocl3gaf  3491  axdc4uz  13077  wrdl3s3  14083  relexpindlem  14179  sqrtval  14353  sqreu  14476  coprmprod  15746  mreexexd  16660  iscatd2  16693  lmodprop2d  19280  neiptopnei  21306  hausnei  21502  isreg2  21551  regr1lem2  21913  ustval  22375  ustuqtop4  22417  axtgupdim2  25782  axtgeucl  25783  iscgra  26117  brbtwn  26197  ax5seg  26236  axlowdim  26259  axeuclidlem  26260  wlkonprop  26954  upgr2wlk  26964  upgrf1istrl  27005  elwspths2spth  27295  clwlkclwwlk  27330  clwlkclwwlkOLD  27331  clwwlknonel  27467  upgr4cycl4dv4e  27560  extwwlkfab  27739  extwwlkfabOLD  27740  nvi  28023  br8d  29968  xlt2addrd  30069  isslmd  30299  slmdlema  30300  tgoldbachgt  31289  axtgupdim2OLD  31294  br8  32187  br6  32188  br4  32189  fvtransport  32677  brcolinear2  32703  colineardim1  32706  fscgr  32725  idinside  32729  brsegle  32753  poimirlem28  33980  caures  34097  iscringd  34338  oposlem  35256  cdleme18d  36369  jm2.27  38417  9gbo  42491  11gbo  42492