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  3537  vtocl3gaOLD  3539  offval22  8021  ereq2  8633  brttrcl  9609  ttrclss  9616  ttrclselem2  9622  wrdl3s3  14869  mhmlem  18941  isdrngrd  20651  isdrngrdOLD  20653  lmodlema  20768  mdetunilem9  22505  neiptoptop  23016  neiptopnei  23017  hausnei  23213  regr1lem2  23625  ustuqtop4  24130  utopsnneiplem  24133  axtg5seg  28410  axtgupdim2  28416  axtgeucl  28417  brbtwn  28844  axlowdim  28906  axeuclidlem  28907  incistruhgr  29024  issubgr2  29217  wwlksnwwlksnon  29860  upgr4cycl4dv4e  30129  isnvlem  30554  csmdsymi  32278  br8d  32555  slmdlema  33145  constrconj  33712  constrllcllem  33719  constrcccllem  33721  constrcbvlem  33722  carsgmon  34282  sitgclg  34310  tgoldbachgt  34631  axtgupdim2ALTV  34636  bnj852  34888  bnj18eq1  34894  bnj938  34904  bnj983  34918  bnj1318  34992  bnj1326  34993  cvmlift3lem4  35295  cvmlift3  35301  br8  35729  br6  35730  br4  35731  brcolinear2  36032  colineardim1  36035  brfs  36053  fscgr  36054  btwnconn1lem7  36067  brsegle  36082  unblimceq0  36481  sdclem2  37722  sdclem1  37723  sdc  37724  fdc  37725  cdleme18d  40274  cdlemk35s  40916  cdlemk39s  40918  monotoddzz  42916  jm2.27  42981  mendlmod  43162  minregex2  43508  fiiuncl  45043  wessf1ornlem  45163  fmulcl  45562  fmuldfeqlem1  45563  fprodcncf  45881  dvmptfprodlem  45925  dvmptfprod  45926  dvnprodlem2  45928  stoweidlem6  45987  stoweidlem8  45989  stoweidlem31  46012  stoweidlem34  46015  stoweidlem43  46024  stoweidlem52  46033  fourierdlem41  46129  fourierdlem48  46135  fourierdlem49  46136  ovnsubaddlem1  46551  ichexmpl2  47454  9gbo  47758  11gbo  47759  lmod1  48477  cnelsubclem  49588