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  8103  ereq2  8733  brttrcl  9721  ttrclss  9728  ttrclselem2  9734  wrdl3s3  15124  mhmlem  19281  isdrngrd  21032  isdrngrdOLD  21034  lmodlema  21149  mdetunilem9  22944  neiptoptop  23458  neiptopnei  23459  hausnei  23655  regr1lem2  24068  ustuqtop4  24572  utopsnneiplem  24575  bdayfinbndlem1  28862  axtg5seg  28936  axtgupdim2  28942  axtgeucl  28943  brbtwn  29486  axlowdim  29548  axeuclidlem  29549  incistruhgr  29666  issubgr2  29862  wwlksnwwlksnon  30513  upgr4cycl4dv4e  30795  isnvlem  31221  csmdsymi  32945  br8d  33253  slmdlema  33814  constrconj  34427  constrllcllem  34434  constrcccllem  34436  constrcbvlem  34437  carsgmon  34996  sitgclg  35024  tgoldbachgt  35342  axtgupdim2ALTV  35347  bnj852  35601  bnj18eq1  35607  bnj938  35617  bnj983  35631  bnj1318  35705  bnj1326  35706  cvmlift3lem4  36177  cvmlift3  36183  mirimanoffr  36550  br8  36617  br6  36618  br4  36619  brcolinear2  36919  colineardim1  36922  brfs  36940  fscgr  36941  btwnconn1lem7  36954  brsegle  36969  unblimceq0  37469  sdclem2  38785  sdclem1  38786  sdc  38787  fdc  38788  cdleme18d  41461  cdlemk35s  42103  cdlemk39s  42105  monotoddzz  44059  jm2.27  44124  mendlmod  44300  minregex2  44645  fiiuncl  46190  wessf1ornlem  46308  fmulcl  46701  fmuldfeqlem1  46702  fprodcncf  47018  dvmptfprodlem  47062  dvmptfprod  47063  dvnprodlem2  47065  stoweidlem6  47124  stoweidlem8  47126  stoweidlem31  47149  stoweidlem34  47152  stoweidlem43  47161  stoweidlem52  47170  fourierdlem41  47266  fourierdlem48  47272  fourierdlem49  47273  ovnsubaddlem1  47688  ichexmpl2  48660  9gbo  48980  11gbo  48981  lmod1  49712  cnelsubcw  50849