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  3545  vtocl3gaOLD  3547  offval22  8044  ereq2  8656  brttrcl  9642  ttrclss  9649  ttrclselem2  9655  wrdl3s3  14904  mhmlem  18970  isdrngrd  20651  isdrngrdOLD  20653  lmodlema  20747  mdetunilem9  22483  neiptoptop  22994  neiptopnei  22995  hausnei  23191  regr1lem2  23603  ustuqtop4  24108  utopsnneiplem  24111  axtg5seg  28368  axtgupdim2  28374  axtgeucl  28375  brbtwn  28802  axlowdim  28864  axeuclidlem  28865  incistruhgr  28982  issubgr2  29175  wwlksnwwlksnon  29818  upgr4cycl4dv4e  30087  isnvlem  30512  csmdsymi  32236  br8d  32511  slmdlema  33129  constrconj  33708  constrllcllem  33715  constrcccllem  33717  constrcbvlem  33718  carsgmon  34278  sitgclg  34306  tgoldbachgt  34627  axtgupdim2ALTV  34632  bnj852  34884  bnj18eq1  34890  bnj938  34900  bnj983  34914  bnj1318  34988  bnj1326  34989  cvmlift3lem4  35282  cvmlift3  35288  br8  35716  br6  35717  br4  35718  brcolinear2  36019  colineardim1  36022  brfs  36040  fscgr  36041  btwnconn1lem7  36054  brsegle  36069  unblimceq0  36468  sdclem2  37709  sdclem1  37710  sdc  37711  fdc  37712  cdleme18d  40262  cdlemk35s  40904  cdlemk39s  40906  monotoddzz  42905  jm2.27  42970  mendlmod  43151  minregex2  43497  fiiuncl  45032  wessf1ornlem  45152  fmulcl  45552  fmuldfeqlem1  45553  fprodcncf  45871  dvmptfprodlem  45915  dvmptfprod  45916  dvnprodlem2  45918  stoweidlem6  45977  stoweidlem8  45979  stoweidlem31  46002  stoweidlem34  46005  stoweidlem43  46014  stoweidlem52  46023  fourierdlem41  46119  fourierdlem48  46125  fourierdlem49  46126  ovnsubaddlem1  46541  ichexmpl2  47444  9gbo  47748  11gbo  47749  lmod1  48454  cnelsubclem  49565