Theorem 3anbi2d 1396

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  vtocl3gaf  3248  offval22  7140  ereq2  7637  wrdl3s3  13553  mhmlem  17358  isdrngrd  18596  lmodlema  18691  mdetunilem9  20245  neiptoptop  20745  neiptopnei  20746  hausnei  20942  regr1lem2  21353  ustuqtop4  21858  utopsnneiplem  21861  axtg5seg  25164  axtgupdim2  25170  axtgeucl  25171  brbtwn  25579  axlowdim  25641  axeuclidlem  25642  incistruhgr  25746  usgra2wlkspthlem1  26147  usgra2wlkspthlem2  26148  el2wlkonot  26396  el2spthonot  26397  el2spthonot0  26398  isnvlem  26849  csmdsymi  28577  br8d  28802  slmdlema  29087  carsgmon  29703  sitgclg  29731  axtgupdim2OLD  29999  bnj852  30245  bnj18eq1  30251  bnj938  30261  bnj983  30275  bnj1318  30347  bnj1326  30348  cvmlift3lem4  30558  cvmlift3  30564  br8  30899  br6  30900  br4  30901  brcolinear2  31335  colineardim1  31338  brfs  31356  fscgr  31357  btwnconn1lem7  31370  brsegle  31385  unblimceq0  31668  sdclem2  32708  sdclem1  32709  sdc  32710  fdc  32711  cdleme18d  34600  cdlemk35s  35243  cdlemk39s  35245  monotoddzz  36526  jm2.27  36593  mendlmod  36782  fiiuncl  38259  wessf1ornlem  38366  fmulcl  38648  fmuldfeqlem1  38649  fprodcncf  38787  dvmptfprodlem  38834  dvmptfprod  38835  dvnprodlem2  38837  stoweidlem6  38899  stoweidlem8  38901  stoweidlem31  38924  stoweidlem34  38927  stoweidlem43  38936  stoweidlem52  38945  fourierdlem41  39041  fourierdlem48  39047  fourierdlem49  39048  ovnsubaddlem1  39460  9gboa  40196  11gboa  40197  issubgr2  40496  wwlksnwwlksnon  41121  upgr4cycl4dv4e  41352  lmod1  42075