Theorem 3anbi1d 1441

Description: Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)

Hypothesis

Ref	Expression
3anbi1d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
3anbi1d	⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜏) ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))

Proof of Theorem 3anbi1d

Step	Hyp	Ref	Expression
1		3anbi1d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		biidd 265	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃))
3	1, 2	3anbi12d 1438	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜏) ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1088

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 210  df-an 400  df-3an 1090

This theorem is referenced by:  vtocl3gaf  3480  axdc4uz  13436  wrdl3s3  14408  relexpindlem  14505  sqrtval  14679  sqreu  14803  coprmprod  16095  mreexexd  17015  iscatd2  17048  lmodprop2d  19808  neiptopnei  21876  hausnei  22072  isreg2  22121  regr1lem2  22484  ustval  22947  ustuqtop4  22989  axtgupdim2  26409  axtgeucl  26410  iscgra  26747  brbtwn  26837  ax5seg  26876  axlowdim  26899  axeuclidlem  26900  wlkonprop  27592  upgr2wlk  27602  upgrf1istrl  27637  elwspths2spth  27897  clwlkclwwlk  27931  clwwlknonel  28024  upgr4cycl4dv4e  28114  extwwlkfab  28281  nvi  28541  br8d  30516  xlt2addrd  30648  isslmd  31024  slmdlema  31025  tgoldbachgt  32205  axtgupdim2ALTV  32210  br8  33287  br6  33288  br4  33289  fvtransport  33964  brcolinear2  33990  colineardim1  33993  fscgr  34012  idinside  34016  brsegle  34040  poimirlem28  35417  caures  35530  iscringd  35768  oposlem  36808  cdleme18d  37921  jm2.27  40386  ichexmpl2  44440  ichnreuop  44442  9gbo  44744  11gbo  44745