Theorem 3anbi2d 1444

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1087

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 1089

This theorem is referenced by:  vtocl3gafOLD  3539  vtocl3gaOLD  3541  offval22  8040  ereq2  8654  brttrcl  9634  ttrclss  9641  ttrclselem2  9647  wrdl3s3  14897  mhmlem  19004  isdrngrd  20711  isdrngrdOLD  20713  lmodlema  20828  mdetunilem9  22576  neiptoptop  23087  neiptopnei  23088  hausnei  23284  regr1lem2  23696  ustuqtop4  24200  utopsnneiplem  24203  bdayfinbndlem1  28475  axtg5seg  28549  axtgupdim2  28555  axtgeucl  28556  brbtwn  28984  axlowdim  29046  axeuclidlem  29047  incistruhgr  29164  issubgr2  29357  wwlksnwwlksnon  30000  upgr4cycl4dv4e  30272  isnvlem  30698  csmdsymi  32422  br8d  32698  slmdlema  33297  constrconj  33923  constrllcllem  33930  constrcccllem  33932  constrcbvlem  33933  carsgmon  34492  sitgclg  34520  tgoldbachgt  34841  axtgupdim2ALTV  34846  bnj852  35097  bnj18eq1  35103  bnj938  35113  bnj983  35127  bnj1318  35201  bnj1326  35202  cvmlift3lem4  35538  cvmlift3  35544  br8  35972  br6  35973  br4  35974  brcolinear2  36274  colineardim1  36277  brfs  36295  fscgr  36296  btwnconn1lem7  36309  brsegle  36324  unblimceq0  36729  sdclem2  37993  sdclem1  37994  sdc  37995  fdc  37996  cdleme18d  40671  cdlemk35s  41313  cdlemk39s  41315  monotoddzz  43300  jm2.27  43365  mendlmod  43546  minregex2  43891  fiiuncl  45425  wessf1ornlem  45544  fmulcl  45941  fmuldfeqlem1  45942  fprodcncf  46258  dvmptfprodlem  46302  dvmptfprod  46303  dvnprodlem2  46305  stoweidlem6  46364  stoweidlem8  46366  stoweidlem31  46389  stoweidlem34  46392  stoweidlem43  46401  stoweidlem52  46410  fourierdlem41  46506  fourierdlem48  46512  fourierdlem49  46513  ovnsubaddlem1  46928  ichexmpl2  47830  9gbo  48134  11gbo  48135  lmod1  48852  cnelsubclem  49962