Theorem 3anbi2d 1469

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 265	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃))
2		3anbi1d.1	. 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:  offval22  8097  ereq2  8719  brttrcl  9707  ttrclss  9714  ttrclselem2  9720  wrdl3s3  15108  mhmlem  19265  isdrngrd  21016  isdrngrdOLD  21018  lmodlema  21133  mdetunilem9  22928  neiptoptop  23442  neiptopnei  23443  hausnei  23639  regr1lem2  24052  ustuqtop4  24556  utopsnneiplem  24559  bdayfinbndlem1  28846  axtg5seg  28920  axtgupdim2  28926  axtgeucl  28927  brbtwn  29470  axlowdim  29532  axeuclidlem  29533  incistruhgr  29650  issubgr2  29846  wwlksnwwlksnon  30497  upgr4cycl4dv4e  30779  isnvlem  31205  csmdsymi  32929  br8d  33195  slmdlema  33757  constrconj  34370  constrllcllem  34377  constrcccllem  34379  constrcbvlem  34380  carsgmon  34939  sitgclg  34967  tgoldbachgt  35285  axtgupdim2ALTV  35290  bnj852  35544  bnj18eq1  35550  bnj938  35560  bnj983  35574  bnj1318  35648  bnj1326  35649  cvmlift3lem4  36066  cvmlift3  36072  br8  36500  br6  36501  br4  36502  brcolinear2  36803  colineardim1  36806  brfs  36824  fscgr  36825  btwnconn1lem7  36838  brsegle  36853  unblimceq0  37353  sdclem2  38656  sdclem1  38657  sdc  38658  fdc  38659  cdleme18d  41332  cdlemk35s  41974  cdlemk39s  41976  monotoddzz  43929  jm2.27  43994  mendlmod  44175  minregex2  44520  fiiuncl  46051  wessf1ornlem  46169  fmulcl  46562  fmuldfeqlem1  46563  fprodcncf  46879  dvmptfprodlem  46923  dvmptfprod  46924  dvnprodlem2  46926  stoweidlem6  46985  stoweidlem8  46987  stoweidlem31  47010  stoweidlem34  47013  stoweidlem43  47022  stoweidlem52  47031  fourierdlem41  47127  fourierdlem48  47133  fourierdlem49  47134  ovnsubaddlem1  47549  ichexmpl2  48521  9gbo  48841  11gbo  48842  lmod1  49573  cnelsubclem  50680