Theorem 3anbi2d 1449

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 263	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃))
2		3anbi1d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	3anbi12d 1445	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓 ∧ 𝜏) ↔ (𝜃 ∧ 𝜒 ∧ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 207   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  offval22  8027  ereq2  8642  brttrcl  9625  ttrclss  9632  ttrclselem2  9638  wrdl3s3  14915  mhmlem  19029  isdrngrd  20738  isdrngrdOLD  20740  lmodlema  20855  mdetunilem9  22603  neiptoptop  23114  neiptopnei  23115  hausnei  23311  regr1lem2  23723  ustuqtop4  24227  utopsnneiplem  24230  bdayfinbndlem1  28477  axtg5seg  28551  axtgupdim2  28557  axtgeucl  28558  brbtwn  28986  axlowdim  29048  axeuclidlem  29049  incistruhgr  29166  issubgr2  29359  wwlksnwwlksnon  30001  upgr4cycl4dv4e  30273  isnvlem  30699  csmdsymi  32423  br8d  32700  slmdlema  33284  constrconj  33929  constrllcllem  33936  constrcccllem  33938  constrcbvlem  33939  carsgmon  34498  sitgclg  34526  tgoldbachgt  34847  axtgupdim2ALTV  34852  bnj852  35103  bnj18eq1  35109  bnj938  35119  bnj983  35133  bnj1318  35207  bnj1326  35208  cvmlift3lem4  35550  cvmlift3  35556  br8  35984  br6  35985  br4  35986  brcolinear2  36286  colineardim1  36289  brfs  36307  fscgr  36308  btwnconn1lem7  36321  brsegle  36336  unblimceq0  36813  sdclem2  38109  sdclem1  38110  sdc  38111  fdc  38112  cdleme18d  40787  cdlemk35s  41429  cdlemk39s  41431  monotoddzz  43388  jm2.27  43453  mendlmod  43634  minregex2  43979  fiiuncl  45513  wessf1ornlem  45632  fmulcl  46026  fmuldfeqlem1  46027  fprodcncf  46343  dvmptfprodlem  46387  dvmptfprod  46388  dvnprodlem2  46390  stoweidlem6  46449  stoweidlem8  46451  stoweidlem31  46474  stoweidlem34  46477  stoweidlem43  46486  stoweidlem52  46495  fourierdlem41  46591  fourierdlem48  46597  fourierdlem49  46598  ovnsubaddlem1  47013  ichexmpl2  47945  9gbo  48265  11gbo  48266  lmod1  48983  cnelsubclem  50093