Theorem 3anbi2d 1552

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ w3a 1071

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 197  df-an 383  df-3an 1073

This theorem is referenced by:  vtocl3gaf  3426  offval22  7403  ereq2  7903  wrdl3s3  13914  mhmlem  17742  isdrngrd  18982  lmodlema  19077  mdetunilem9  20643  neiptoptop  21155  neiptopnei  21156  hausnei  21352  regr1lem2  21763  ustuqtop4  22267  utopsnneiplem  22270  axtg5seg  25584  axtgupdim2  25590  axtgeucl  25591  brbtwn  25999  axlowdim  26061  axeuclidlem  26062  incistruhgr  26194  issubgr2  26386  wwlksnwwlksnon  27059  wwlksnwwlksnonOLD  27061  upgr4cycl4dv4e  27364  isnvlem  27802  csmdsymi  29530  br8d  29757  slmdlema  30093  carsgmon  30713  sitgclg  30741  tgoldbachgt  31078  axtgupdim2OLD  31083  bnj852  31326  bnj18eq1  31332  bnj938  31342  bnj983  31356  bnj1318  31428  bnj1326  31429  cvmlift3lem4  31639  cvmlift3  31645  br8  31981  br6  31982  br4  31983  brcolinear2  32499  colineardim1  32502  brfs  32520  fscgr  32521  btwnconn1lem7  32534  brsegle  32549  unblimceq0  32832  sdclem2  33866  sdclem1  33867  sdc  33868  fdc  33869  cdleme18d  36100  cdlemk35s  36742  cdlemk39s  36744  monotoddzz  38030  jm2.27  38097  mendlmod  38285  fiiuncl  39751  wessf1ornlem  39887  fmulcl  40327  fmuldfeqlem1  40328  fprodcncf  40628  dvmptfprodlem  40673  dvmptfprod  40674  dvnprodlem2  40676  stoweidlem6  40736  stoweidlem8  40738  stoweidlem31  40761  stoweidlem34  40764  stoweidlem43  40773  stoweidlem52  40782  fourierdlem41  40878  fourierdlem48  40884  fourierdlem49  40885  ovnsubaddlem1  41300  9gbo  42186  11gbo  42187  lmod1  42805