Theorem 3anbi2d 1441

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 1437	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓 ∧ 𝜏) ↔ (𝜃 ∧ 𝜒 ∧ 𝜏)))

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

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 397  df-3an 1089

This theorem is referenced by:  vtocl3gaf  3568  vtocl3ga  3569  offval22  8076  ereq2  8713  brttrcl  9710  ttrclss  9717  ttrclselem2  9723  wrdl3s3  14917  mhmlem  18981  isdrngrd  20534  isdrngrdOLD  20536  lmodlema  20619  mdetunilem9  22342  neiptoptop  22855  neiptopnei  22856  hausnei  23052  regr1lem2  23464  ustuqtop4  23969  utopsnneiplem  23972  axtg5seg  27971  axtgupdim2  27977  axtgeucl  27978  brbtwn  28412  axlowdim  28474  axeuclidlem  28475  incistruhgr  28594  issubgr2  28784  wwlksnwwlksnon  29424  upgr4cycl4dv4e  29693  isnvlem  30118  csmdsymi  31842  br8d  32094  slmdlema  32606  carsgmon  33599  sitgclg  33627  tgoldbachgt  33961  axtgupdim2ALTV  33966  bnj852  34218  bnj18eq1  34224  bnj938  34234  bnj983  34248  bnj1318  34322  bnj1326  34323  cvmlift3lem4  34599  cvmlift3  34605  br8  35018  br6  35019  br4  35020  brcolinear2  35322  colineardim1  35325  brfs  35343  fscgr  35344  btwnconn1lem7  35357  brsegle  35372  unblimceq0  35686  sdclem2  36913  sdclem1  36914  sdc  36915  fdc  36916  cdleme18d  39469  cdlemk35s  40111  cdlemk39s  40113  monotoddzz  41984  jm2.27  42049  mendlmod  42237  minregex2  42588  fiiuncl  44054  wessf1ornlem  44183  fmulcl  44596  fmuldfeqlem1  44597  fprodcncf  44915  dvmptfprodlem  44959  dvmptfprod  44960  dvnprodlem2  44962  stoweidlem6  45021  stoweidlem8  45023  stoweidlem31  45046  stoweidlem34  45049  stoweidlem43  45058  stoweidlem52  45067  fourierdlem41  45163  fourierdlem48  45169  fourierdlem49  45170  ovnsubaddlem1  45585  ichexmpl2  46437  9gbo  46741  11gbo  46742  lmod1  47261