Theorem 3anbi2d 1469

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 1465	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  8089  ereq2  8709  brttrcl  9689  ttrclss  9696  ttrclselem2  9702  wrdl3s3  15023  mhmlem  19172  isdrngrd  20919  isdrngrdOLD  20921  lmodlema  21036  mdetunilem9  22827  neiptoptop  23338  neiptopnei  23339  hausnei  23535  regr1lem2  23948  ustuqtop4  24452  utopsnneiplem  24455  bdayfinbndlem1  28711  axtg5seg  28785  axtgupdim2  28791  axtgeucl  28792  brbtwn  29304  axlowdim  29366  axeuclidlem  29367  incistruhgr  29484  issubgr2  29680  wwlksnwwlksnon  30331  upgr4cycl4dv4e  30607  isnvlem  31033  csmdsymi  32757  br8d  33024  slmdlema  33587  constrconj  34199  constrllcllem  34206  constrcccllem  34208  constrcbvlem  34209  carsgmon  34769  sitgclg  34797  tgoldbachgt  35115  axtgupdim2ALTV  35120  bnj852  35374  bnj18eq1  35380  bnj938  35390  bnj983  35404  bnj1318  35478  bnj1326  35479  cvmlift3lem4  35851  cvmlift3  35857  br8  36285  br6  36286  br4  36287  brcolinear2  36587  colineardim1  36590  brfs  36608  fscgr  36609  btwnconn1lem7  36622  brsegle  36637  unblimceq0  37153  sdclem2  38451  sdclem1  38452  sdc  38453  fdc  38454  cdleme18d  41127  cdlemk35s  41769  cdlemk39s  41771  monotoddzz  43728  jm2.27  43793  mendlmod  43974  minregex2  44319  fiiuncl  45843  wessf1ornlem  45961  fmulcl  46355  fmuldfeqlem1  46356  fprodcncf  46672  dvmptfprodlem  46716  dvmptfprod  46717  dvnprodlem2  46719  stoweidlem6  46778  stoweidlem8  46780  stoweidlem31  46803  stoweidlem34  46806  stoweidlem43  46815  stoweidlem52  46824  fourierdlem41  46920  fourierdlem48  46926  fourierdlem49  46927  ovnsubaddlem1  47342  ichexmpl2  48277  9gbo  48597  11gbo  48598  lmod1  49329  cnelsubclem  50438