Theorem 3anbi2d 1437

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  vtocl3gaf  3579  offval22  7785  ereq2  8299  wrdl3s3  14328  mhmlem  18221  isdrngrd  19530  lmodlema  19641  mdetunilem9  21231  neiptoptop  21741  neiptopnei  21742  hausnei  21938  regr1lem2  22350  ustuqtop4  22855  utopsnneiplem  22858  axtg5seg  26253  axtgupdim2  26259  axtgeucl  26260  brbtwn  26687  axlowdim  26749  axeuclidlem  26750  incistruhgr  26866  issubgr2  27056  wwlksnwwlksnon  27696  upgr4cycl4dv4e  27966  isnvlem  28389  csmdsymi  30113  br8d  30363  slmdlema  30833  carsgmon  31574  sitgclg  31602  tgoldbachgt  31936  axtgupdim2ALTV  31941  bnj852  32195  bnj18eq1  32201  bnj938  32211  bnj983  32225  bnj1318  32299  bnj1326  32300  cvmlift3lem4  32571  cvmlift3  32577  br8  32994  br6  32995  br4  32996  brcolinear2  33521  colineardim1  33524  brfs  33542  fscgr  33543  btwnconn1lem7  33556  brsegle  33571  unblimceq0  33848  sdclem2  35019  sdclem1  35020  sdc  35021  fdc  35022  cdleme18d  37433  cdlemk35s  38075  cdlemk39s  38077  monotoddzz  39547  jm2.27  39612  mendlmod  39800  fiiuncl  41334  wessf1ornlem  41452  fmulcl  41869  fmuldfeqlem1  41870  fprodcncf  42191  dvmptfprodlem  42236  dvmptfprod  42237  dvnprodlem2  42239  stoweidlem6  42298  stoweidlem8  42300  stoweidlem31  42323  stoweidlem34  42326  stoweidlem43  42335  stoweidlem52  42344  fourierdlem41  42440  fourierdlem48  42446  fourierdlem49  42447  ovnsubaddlem1  42859  ichexmpl2  43639  9gbo  43946  11gbo  43947  lmod1  44554