Theorem 3anbi2d 1441

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 1437	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓 ∧ 𝜏) ↔ (𝜃 ∧ 𝜒 ∧ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1087

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 1089

This theorem is referenced by:  vtocl3gaf  3535  vtocl3ga  3536  offval22  8012  ereq2  8614  brttrcl  9607  ttrclss  9614  ttrclselem2  9620  wrdl3s3  14811  mhmlem  18826  isdrngrd  20168  lmodlema  20280  mdetunilem9  21921  neiptoptop  22434  neiptopnei  22435  hausnei  22631  regr1lem2  23043  ustuqtop4  23548  utopsnneiplem  23551  axtg5seg  27236  axtgupdim2  27242  axtgeucl  27243  brbtwn  27677  axlowdim  27739  axeuclidlem  27740  incistruhgr  27859  issubgr2  28049  wwlksnwwlksnon  28689  upgr4cycl4dv4e  28958  isnvlem  29381  csmdsymi  31105  br8d  31358  slmdlema  31864  carsgmon  32726  sitgclg  32754  tgoldbachgt  33088  axtgupdim2ALTV  33093  bnj852  33345  bnj18eq1  33351  bnj938  33361  bnj983  33375  bnj1318  33449  bnj1326  33450  cvmlift3lem4  33728  cvmlift3  33734  br8  34145  br6  34146  br4  34147  brcolinear2  34581  colineardim1  34584  brfs  34602  fscgr  34603  btwnconn1lem7  34616  brsegle  34631  unblimceq0  34908  sdclem2  36139  sdclem1  36140  sdc  36141  fdc  36142  cdleme18d  38696  cdlemk35s  39338  cdlemk39s  39340  monotoddzz  41176  jm2.27  41241  mendlmod  41429  minregex2  41718  fiiuncl  43184  wessf1ornlem  43308  fmulcl  43723  fmuldfeqlem1  43724  fprodcncf  44042  dvmptfprodlem  44086  dvmptfprod  44087  dvnprodlem2  44089  stoweidlem6  44148  stoweidlem8  44150  stoweidlem31  44173  stoweidlem34  44176  stoweidlem43  44185  stoweidlem52  44194  fourierdlem41  44290  fourierdlem48  44296  fourierdlem49  44297  ovnsubaddlem1  44712  ichexmpl2  45563  9gbo  45867  11gbo  45868  lmod1  46474