Theorem 3anbi2d 1467

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  offval22  8082  ereq2  8702  brttrcl  9681  ttrclss  9688  ttrclselem2  9694  wrdl3s3  14998  mhmlem  19127  isdrngrd  20847  isdrngrdOLD  20849  lmodlema  20963  mdetunilem9  22745  neiptoptop  23256  neiptopnei  23257  hausnei  23453  regr1lem2  23865  ustuqtop4  24369  utopsnneiplem  24372  bdayfinbndlem1  28625  axtg5seg  28699  axtgupdim2  28705  axtgeucl  28706  brbtwn  29189  axlowdim  29251  axeuclidlem  29252  incistruhgr  29369  issubgr2  29562  wwlksnwwlksnon  30204  upgr4cycl4dv4e  30476  isnvlem  30902  csmdsymi  32626  br8d  32893  slmdlema  33463  constrconj  34079  constrllcllem  34086  constrcccllem  34088  constrcbvlem  34089  carsgmon  34648  sitgclg  34676  tgoldbachgt  34994  axtgupdim2ALTV  34999  bnj852  35253  bnj18eq1  35259  bnj938  35269  bnj983  35283  bnj1318  35357  bnj1326  35358  cvmlift3lem4  35712  cvmlift3  35718  br8  36146  br6  36147  br4  36148  brcolinear2  36448  colineardim1  36451  brfs  36469  fscgr  36470  btwnconn1lem7  36483  brsegle  36498  unblimceq0  36984  sdclem2  38280  sdclem1  38281  sdc  38282  fdc  38283  cdleme18d  40958  cdlemk35s  41600  cdlemk39s  41602  monotoddzz  43561  jm2.27  43626  mendlmod  43807  minregex2  44152  fiiuncl  45676  wessf1ornlem  45794  fmulcl  46188  fmuldfeqlem1  46189  fprodcncf  46505  dvmptfprodlem  46549  dvmptfprod  46550  dvnprodlem2  46552  stoweidlem6  46611  stoweidlem8  46613  stoweidlem31  46636  stoweidlem34  46639  stoweidlem43  46648  stoweidlem52  46657  fourierdlem41  46753  fourierdlem48  46759  fourierdlem49  46760  ovnsubaddlem1  47175  ichexmpl2  48107  9gbo  48427  11gbo  48428  lmod1  49156  cnelsubclem  50265