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 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  3582  vtocl3gaOLD  3584  offval22  8113  ereq2  8753  brttrcl  9753  ttrclss  9760  ttrclselem2  9766  wrdl3s3  15001  mhmlem  19080  isdrngrd  20766  isdrngrdOLD  20768  lmodlema  20863  mdetunilem9  22626  neiptoptop  23139  neiptopnei  23140  hausnei  23336  regr1lem2  23748  ustuqtop4  24253  utopsnneiplem  24256  axtg5seg  28473  axtgupdim2  28479  axtgeucl  28480  brbtwn  28914  axlowdim  28976  axeuclidlem  28977  incistruhgr  29096  issubgr2  29289  wwlksnwwlksnon  29935  upgr4cycl4dv4e  30204  isnvlem  30629  csmdsymi  32353  br8d  32622  slmdlema  33209  constrconj  33786  carsgmon  34316  sitgclg  34344  tgoldbachgt  34678  axtgupdim2ALTV  34683  bnj852  34935  bnj18eq1  34941  bnj938  34951  bnj983  34965  bnj1318  35039  bnj1326  35040  cvmlift3lem4  35327  cvmlift3  35333  br8  35756  br6  35757  br4  35758  brcolinear2  36059  colineardim1  36062  brfs  36080  fscgr  36081  btwnconn1lem7  36094  brsegle  36109  unblimceq0  36508  sdclem2  37749  sdclem1  37750  sdc  37751  fdc  37752  cdleme18d  40297  cdlemk35s  40939  cdlemk39s  40941  monotoddzz  42955  jm2.27  43020  mendlmod  43201  minregex2  43548  fiiuncl  45070  wessf1ornlem  45190  fmulcl  45596  fmuldfeqlem1  45597  fprodcncf  45915  dvmptfprodlem  45959  dvmptfprod  45960  dvnprodlem2  45962  stoweidlem6  46021  stoweidlem8  46023  stoweidlem31  46046  stoweidlem34  46049  stoweidlem43  46058  stoweidlem52  46067  fourierdlem41  46163  fourierdlem48  46169  fourierdlem49  46170  ovnsubaddlem1  46585  ichexmpl2  47457  9gbo  47761  11gbo  47762  lmod1  48409