Theorem 3anbi2d 1558

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

Syntax hints:   → wi 4   ↔ wb 197   ∧ w3a 1100

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 198  df-an 385  df-3an 1102

This theorem is referenced by:  vtocl3gaf  3468  offval22  7483  ereq2  7983  wrdl3s3  13926  mhmlem  17736  isdrngrd  18973  lmodlema  19068  mdetunilem9  20634  neiptoptop  21146  neiptopnei  21147  hausnei  21343  regr1lem2  21754  ustuqtop4  22258  utopsnneiplem  22261  axtg5seg  25577  axtgupdim2  25583  axtgeucl  25584  brbtwn  25992  axlowdim  26054  axeuclidlem  26055  incistruhgr  26187  issubgr2  26379  wwlksnwwlksnon  27052  wwlksnwwlksnonOLD  27054  upgr4cycl4dv4e  27357  isnvlem  27792  csmdsymi  29520  br8d  29746  slmdlema  30080  carsgmon  30700  sitgclg  30728  tgoldbachgt  31065  axtgupdim2OLD  31070  bnj852  31312  bnj18eq1  31318  bnj938  31328  bnj983  31342  bnj1318  31414  bnj1326  31415  cvmlift3lem4  31625  cvmlift3  31631  br8  31966  br6  31967  br4  31968  brcolinear2  32484  colineardim1  32487  brfs  32505  fscgr  32506  btwnconn1lem7  32519  brsegle  32534  unblimceq0  32813  sdclem2  33847  sdclem1  33848  sdc  33849  fdc  33850  cdleme18d  36073  cdlemk35s  36715  cdlemk39s  36717  monotoddzz  38006  jm2.27  38073  mendlmod  38261  fiiuncl  39724  wessf1ornlem  39857  fmulcl  40290  fmuldfeqlem1  40291  fprodcncf  40591  dvmptfprodlem  40636  dvmptfprod  40637  dvnprodlem2  40639  stoweidlem6  40699  stoweidlem8  40701  stoweidlem31  40724  stoweidlem34  40727  stoweidlem43  40736  stoweidlem52  40745  fourierdlem41  40841  fourierdlem48  40847  fourierdlem49  40848  ovnsubaddlem1  41263  9gbo  42234  11gbo  42235  lmod1  42846