Theorem 3anbi2d 1469

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

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

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 401  df-3an 1105

This theorem is referenced by:  offval22  8079  ereq2  8699  brttrcl  9678  ttrclss  9685  ttrclselem2  9691  wrdl3s3  14995  mhmlem  19123  isdrngrd  20869  isdrngrdOLD  20871  lmodlema  20986  mdetunilem9  22777  neiptoptop  23288  neiptopnei  23289  hausnei  23485  regr1lem2  23897  ustuqtop4  24401  utopsnneiplem  24404  bdayfinbndlem1  28660  axtg5seg  28734  axtgupdim2  28740  axtgeucl  28741  brbtwn  29249  axlowdim  29311  axeuclidlem  29312  incistruhgr  29429  issubgr2  29622  wwlksnwwlksnon  30264  upgr4cycl4dv4e  30536  isnvlem  30962  csmdsymi  32686  br8d  32953  slmdlema  33523  constrconj  34135  constrllcllem  34142  constrcccllem  34144  constrcbvlem  34145  carsgmon  34704  sitgclg  34732  tgoldbachgt  35050  axtgupdim2ALTV  35055  bnj852  35309  bnj18eq1  35315  bnj938  35325  bnj983  35339  bnj1318  35413  bnj1326  35414  cvmlift3lem4  35814  cvmlift3  35820  br8  36248  br6  36249  br4  36250  brcolinear2  36550  colineardim1  36553  brfs  36571  fscgr  36572  btwnconn1lem7  36585  brsegle  36600  unblimceq0  37096  sdclem2  38393  sdclem1  38394  sdc  38395  fdc  38396  cdleme18d  41069  cdlemk35s  41711  cdlemk39s  41713  monotoddzz  43670  jm2.27  43735  mendlmod  43916  minregex2  44261  fiiuncl  45785  wessf1ornlem  45903  fmulcl  46297  fmuldfeqlem1  46298  fprodcncf  46614  dvmptfprodlem  46658  dvmptfprod  46659  dvnprodlem2  46661  stoweidlem6  46720  stoweidlem8  46722  stoweidlem31  46745  stoweidlem34  46748  stoweidlem43  46757  stoweidlem52  46766  fourierdlem41  46862  fourierdlem48  46868  fourierdlem49  46869  ovnsubaddlem1  47284  ichexmpl2  48219  9gbo  48539  11gbo  48540  lmod1  49272  cnelsubclem  50381