Theorem 3anbi2d 1444

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  vtocl3gafOLD  3539  vtocl3gaOLD  3541  offval22  8042  ereq2  8656  brttrcl  9636  ttrclss  9643  ttrclselem2  9649  wrdl3s3  14899  mhmlem  19009  isdrngrd  20716  isdrngrdOLD  20718  lmodlema  20833  mdetunilem9  22581  neiptoptop  23092  neiptopnei  23093  hausnei  23289  regr1lem2  23701  ustuqtop4  24205  utopsnneiplem  24208  bdayfinbndlem1  28480  axtg5seg  28555  axtgupdim2  28561  axtgeucl  28562  brbtwn  28990  axlowdim  29052  axeuclidlem  29053  incistruhgr  29170  issubgr2  29363  wwlksnwwlksnon  30006  upgr4cycl4dv4e  30278  isnvlem  30704  csmdsymi  32428  br8d  32704  slmdlema  33303  constrconj  33929  constrllcllem  33936  constrcccllem  33938  constrcbvlem  33939  carsgmon  34498  sitgclg  34526  tgoldbachgt  34847  axtgupdim2ALTV  34852  bnj852  35103  bnj18eq1  35109  bnj938  35119  bnj983  35133  bnj1318  35207  bnj1326  35208  cvmlift3lem4  35544  cvmlift3  35550  br8  35978  br6  35979  br4  35980  brcolinear2  36280  colineardim1  36283  brfs  36301  fscgr  36302  btwnconn1lem7  36315  brsegle  36330  unblimceq0  36735  sdclem2  38022  sdclem1  38023  sdc  38024  fdc  38025  cdleme18d  40700  cdlemk35s  41342  cdlemk39s  41344  monotoddzz  43329  jm2.27  43394  mendlmod  43575  minregex2  43920  fiiuncl  45454  wessf1ornlem  45573  fmulcl  45970  fmuldfeqlem1  45971  fprodcncf  46287  dvmptfprodlem  46331  dvmptfprod  46332  dvnprodlem2  46334  stoweidlem6  46393  stoweidlem8  46395  stoweidlem31  46418  stoweidlem34  46421  stoweidlem43  46430  stoweidlem52  46439  fourierdlem41  46535  fourierdlem48  46541  fourierdlem49  46542  ovnsubaddlem1  46957  ichexmpl2  47859  9gbo  48163  11gbo  48164  lmod1  48881  cnelsubclem  49991