Theorem 3anbi2d 1438

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  vtocl3gafOLD  3563  vtocl3gaOLD  3565  offval22  8102  ereq2  8742  brttrcl  9756  ttrclss  9763  ttrclselem2  9769  wrdl3s3  14971  mhmlem  19056  isdrngrd  20744  isdrngrdOLD  20746  lmodlema  20841  mdetunilem9  22613  neiptoptop  23126  neiptopnei  23127  hausnei  23323  regr1lem2  23735  ustuqtop4  24240  utopsnneiplem  24243  axtg5seg  28392  axtgupdim2  28398  axtgeucl  28399  brbtwn  28833  axlowdim  28895  axeuclidlem  28896  incistruhgr  29015  issubgr2  29208  wwlksnwwlksnon  29849  upgr4cycl4dv4e  30118  isnvlem  30543  csmdsymi  32267  br8d  32530  slmdlema  33067  constrconj  33603  carsgmon  34148  sitgclg  34176  tgoldbachgt  34509  axtgupdim2ALTV  34514  bnj852  34766  bnj18eq1  34772  bnj938  34782  bnj983  34796  bnj1318  34870  bnj1326  34871  cvmlift3lem4  35150  cvmlift3  35156  br8  35578  br6  35579  br4  35580  brcolinear2  35882  colineardim1  35885  brfs  35903  fscgr  35904  btwnconn1lem7  35917  brsegle  35932  unblimceq0  36210  sdclem2  37443  sdclem1  37444  sdc  37445  fdc  37446  cdleme18d  39994  cdlemk35s  40636  cdlemk39s  40638  monotoddzz  42601  jm2.27  42666  mendlmod  42854  minregex2  43202  fiiuncl  44666  wessf1ornlem  44792  fmulcl  45202  fmuldfeqlem1  45203  fprodcncf  45521  dvmptfprodlem  45565  dvmptfprod  45566  dvnprodlem2  45568  stoweidlem6  45627  stoweidlem8  45629  stoweidlem31  45652  stoweidlem34  45655  stoweidlem43  45664  stoweidlem52  45673  fourierdlem41  45769  fourierdlem48  45775  fourierdlem49  45776  ovnsubaddlem1  46191  ichexmpl2  47042  9gbo  47346  11gbo  47347  lmod1  47875