Theorem 3anbi2d 1440

Description: Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)

Hypothesis

Ref	Expression
3anbi1d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
3anbi2d	⊢ (𝜑 → ((𝜃 ∧ 𝜓 ∧ 𝜏) ↔ (𝜃 ∧ 𝜒 ∧ 𝜏)))

Proof of Theorem 3anbi2d

Step	Hyp	Ref	Expression
1		biidd 261	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃))
2		3anbi1d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	3anbi12d 1436	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓 ∧ 𝜏) ↔ (𝜃 ∧ 𝜒 ∧ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  vtocl3gaf  3517  vtocl3ga  3518  offval22  7937  ereq2  8515  brttrcl  9480  ttrclss  9487  ttrclselem2  9493  wrdl3s3  14686  mhmlem  18704  isdrngrd  20026  lmodlema  20137  mdetunilem9  21778  neiptoptop  22291  neiptopnei  22292  hausnei  22488  regr1lem2  22900  ustuqtop4  23405  utopsnneiplem  23408  axtg5seg  26835  axtgupdim2  26841  axtgeucl  26842  brbtwn  27276  axlowdim  27338  axeuclidlem  27339  incistruhgr  27458  issubgr2  27648  wwlksnwwlksnon  28289  upgr4cycl4dv4e  28558  isnvlem  28981  csmdsymi  30705  br8d  30959  slmdlema  31465  carsgmon  32290  sitgclg  32318  tgoldbachgt  32652  axtgupdim2ALTV  32657  bnj852  32910  bnj18eq1  32916  bnj938  32926  bnj983  32940  bnj1318  33014  bnj1326  33015  cvmlift3lem4  33293  cvmlift3  33299  br8  33732  br6  33733  br4  33734  brcolinear2  34369  colineardim1  34372  brfs  34390  fscgr  34391  btwnconn1lem7  34404  brsegle  34419  unblimceq0  34696  sdclem2  35909  sdclem1  35910  sdc  35911  fdc  35912  cdleme18d  38316  cdlemk35s  38958  cdlemk39s  38960  monotoddzz  40772  jm2.27  40837  mendlmod  41025  minregex2  41149  fiiuncl  42620  wessf1ornlem  42729  fmulcl  43129  fmuldfeqlem1  43130  fprodcncf  43448  dvmptfprodlem  43492  dvmptfprod  43493  dvnprodlem2  43495  stoweidlem6  43554  stoweidlem8  43556  stoweidlem31  43579  stoweidlem34  43582  stoweidlem43  43591  stoweidlem52  43600  fourierdlem41  43696  fourierdlem48  43702  fourierdlem49  43703  ovnsubaddlem1  44115  ichexmpl2  44933  9gbo  45237  11gbo  45238  lmod1  45844