Theorem 3anbi2d 1442

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 398  df-3an 1090

This theorem is referenced by:  vtocl3gaf  3569  vtocl3ga  3570  offval22  8074  ereq2  8711  brttrcl  9708  ttrclss  9715  ttrclselem2  9721  wrdl3s3  14913  mhmlem  18945  isdrngrd  20391  isdrngrdOLD  20393  lmodlema  20476  mdetunilem9  22122  neiptoptop  22635  neiptopnei  22636  hausnei  22832  regr1lem2  23244  ustuqtop4  23749  utopsnneiplem  23752  axtg5seg  27716  axtgupdim2  27722  axtgeucl  27723  brbtwn  28157  axlowdim  28219  axeuclidlem  28220  incistruhgr  28339  issubgr2  28529  wwlksnwwlksnon  29169  upgr4cycl4dv4e  29438  isnvlem  29863  csmdsymi  31587  br8d  31839  slmdlema  32348  carsgmon  33313  sitgclg  33341  tgoldbachgt  33675  axtgupdim2ALTV  33680  bnj852  33932  bnj18eq1  33938  bnj938  33948  bnj983  33962  bnj1318  34036  bnj1326  34037  cvmlift3lem4  34313  cvmlift3  34319  br8  34726  br6  34727  br4  34728  brcolinear2  35030  colineardim1  35033  brfs  35051  fscgr  35052  btwnconn1lem7  35065  brsegle  35080  unblimceq0  35383  sdclem2  36610  sdclem1  36611  sdc  36612  fdc  36613  cdleme18d  39166  cdlemk35s  39808  cdlemk39s  39810  monotoddzz  41682  jm2.27  41747  mendlmod  41935  minregex2  42286  fiiuncl  43752  wessf1ornlem  43882  fmulcl  44297  fmuldfeqlem1  44298  fprodcncf  44616  dvmptfprodlem  44660  dvmptfprod  44661  dvnprodlem2  44663  stoweidlem6  44722  stoweidlem8  44724  stoweidlem31  44747  stoweidlem34  44750  stoweidlem43  44759  stoweidlem52  44768  fourierdlem41  44864  fourierdlem48  44870  fourierdlem49  44871  ovnsubaddlem1  45286  ichexmpl2  46138  9gbo  46442  11gbo  46443  lmod1  47173