Theorem 3anbi2d 1443

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

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

This theorem is referenced by:  vtocl3gafOLD  3551  vtocl3gaOLD  3553  offval22  8070  ereq2  8682  brttrcl  9673  ttrclss  9680  ttrclselem2  9686  wrdl3s3  14935  mhmlem  19001  isdrngrd  20682  isdrngrdOLD  20684  lmodlema  20778  mdetunilem9  22514  neiptoptop  23025  neiptopnei  23026  hausnei  23222  regr1lem2  23634  ustuqtop4  24139  utopsnneiplem  24142  axtg5seg  28399  axtgupdim2  28405  axtgeucl  28406  brbtwn  28833  axlowdim  28895  axeuclidlem  28896  incistruhgr  29013  issubgr2  29206  wwlksnwwlksnon  29852  upgr4cycl4dv4e  30121  isnvlem  30546  csmdsymi  32270  br8d  32545  slmdlema  33163  constrconj  33742  constrllcllem  33749  constrcccllem  33751  constrcbvlem  33752  carsgmon  34312  sitgclg  34340  tgoldbachgt  34661  axtgupdim2ALTV  34666  bnj852  34918  bnj18eq1  34924  bnj938  34934  bnj983  34948  bnj1318  35022  bnj1326  35023  cvmlift3lem4  35316  cvmlift3  35322  br8  35750  br6  35751  br4  35752  brcolinear2  36053  colineardim1  36056  brfs  36074  fscgr  36075  btwnconn1lem7  36088  brsegle  36103  unblimceq0  36502  sdclem2  37743  sdclem1  37744  sdc  37745  fdc  37746  cdleme18d  40296  cdlemk35s  40938  cdlemk39s  40940  monotoddzz  42939  jm2.27  43004  mendlmod  43185  minregex2  43531  fiiuncl  45066  wessf1ornlem  45186  fmulcl  45586  fmuldfeqlem1  45587  fprodcncf  45905  dvmptfprodlem  45949  dvmptfprod  45950  dvnprodlem2  45952  stoweidlem6  46011  stoweidlem8  46013  stoweidlem31  46036  stoweidlem34  46039  stoweidlem43  46048  stoweidlem52  46057  fourierdlem41  46153  fourierdlem48  46159  fourierdlem49  46160  ovnsubaddlem1  46575  ichexmpl2  47475  9gbo  47779  11gbo  47780  lmod1  48485  cnelsubclem  49596