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 262	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃))
2		3anbi1d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	3anbi12d 1437	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  3594  vtocl3gaOLD  3596  offval22  8129  ereq2  8771  brttrcl  9782  ttrclss  9789  ttrclselem2  9795  wrdl3s3  15011  mhmlem  19102  isdrngrd  20788  isdrngrdOLD  20790  lmodlema  20885  mdetunilem9  22647  neiptoptop  23160  neiptopnei  23161  hausnei  23357  regr1lem2  23769  ustuqtop4  24274  utopsnneiplem  24277  axtg5seg  28491  axtgupdim2  28497  axtgeucl  28498  brbtwn  28932  axlowdim  28994  axeuclidlem  28995  incistruhgr  29114  issubgr2  29307  wwlksnwwlksnon  29948  upgr4cycl4dv4e  30217  isnvlem  30642  csmdsymi  32366  br8d  32632  slmdlema  33182  constrconj  33735  carsgmon  34279  sitgclg  34307  tgoldbachgt  34640  axtgupdim2ALTV  34645  bnj852  34897  bnj18eq1  34903  bnj938  34913  bnj983  34927  bnj1318  35001  bnj1326  35002  cvmlift3lem4  35290  cvmlift3  35296  br8  35718  br6  35719  br4  35720  brcolinear2  36022  colineardim1  36025  brfs  36043  fscgr  36044  btwnconn1lem7  36057  brsegle  36072  unblimceq0  36473  sdclem2  37702  sdclem1  37703  sdc  37704  fdc  37705  cdleme18d  40252  cdlemk35s  40894  cdlemk39s  40896  monotoddzz  42900  jm2.27  42965  mendlmod  43150  minregex2  43497  fiiuncl  44967  wessf1ornlem  45092  fmulcl  45502  fmuldfeqlem1  45503  fprodcncf  45821  dvmptfprodlem  45865  dvmptfprod  45866  dvnprodlem2  45868  stoweidlem6  45927  stoweidlem8  45929  stoweidlem31  45952  stoweidlem34  45955  stoweidlem43  45964  stoweidlem52  45973  fourierdlem41  46069  fourierdlem48  46075  fourierdlem49  46076  ovnsubaddlem1  46491  ichexmpl2  47344  9gbo  47648  11gbo  47649  lmod1  48221