Theorem 3anbi2d 1470

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  offval22  8134  ereq2  8764  brttrcl  9751  ttrclss  9758  ttrclselem2  9764  wrdl3s3  15158  mhmlem  19322  isdrngrd  21074  isdrngrdOLD  21076  lmodlema  21191  mdetunilem9  22990  neiptoptop  23504  neiptopnei  23505  hausnei  23701  regr1lem2  24114  ustuqtop4  24618  utopsnneiplem  24621  bdayfinbndlem1  28910  axtg5seg  28984  axtgupdim2  28990  axtgeucl  28991  brbtwn  29534  axlowdim  29596  axeuclidlem  29597  incistruhgr  29714  issubgr2  29910  wwlksnwwlksnon  30561  upgr4cycl4dv4e  30843  isnvlem  31269  csmdsymi  32993  br8d  33300  slmdlema  33863  constrconj  34488  constrllcllem  34495  constrcccllem  34497  constrcbvlem  34498  carsgmon  35057  sitgclg  35085  tgoldbachgt  35403  axtgupdim2ALTV  35408  bnj852  35662  bnj18eq1  35668  bnj938  35678  bnj983  35692  bnj1318  35766  bnj1326  35767  cvmlift3lem4  36295  cvmlift3  36301  mirimanoffr  36668  br8  36736  br6  36737  br4  36738  brcolinear2  37038  colineardim1  37041  brfs  37059  fscgr  37060  btwnconn1lem7  37073  brsegle  37088  unblimceq0  37588  sdclem2  38942  sdclem1  38943  sdc  38944  fdc  38945  cdleme18d  41618  cdlemk35s  42260  cdlemk39s  42262  monotoddzz  44216  jm2.27  44281  mendlmod  44452  minregex2  44797  fiiuncl  46356  wessf1ornlem  46473  fmulcl  46866  fmuldfeqlem1  46867  fprodcncf  47183  dvmptfprodlem  47227  dvmptfprod  47228  dvnprodlem2  47230  stoweidlem6  47289  stoweidlem8  47291  stoweidlem31  47314  stoweidlem34  47317  stoweidlem43  47326  stoweidlem52  47335  fourierdlem41  47431  fourierdlem48  47437  fourierdlem49  47438  ovnsubaddlem1  47853  ichexmpl2  48825  9gbo  49145  11gbo  49146  lmod1  49935  cnelsubcw  51072