Theorem 3anbi2d 1443

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  vtocl3gafOLD  3537  vtocl3gaOLD  3539  offval22  8030  ereq2  8643  brttrcl  9622  ttrclss  9629  ttrclselem2  9635  wrdl3s3  14885  mhmlem  18992  isdrngrd  20699  isdrngrdOLD  20701  lmodlema  20816  mdetunilem9  22564  neiptoptop  23075  neiptopnei  23076  hausnei  23272  regr1lem2  23684  ustuqtop4  24188  utopsnneiplem  24191  bdayfinbndlem1  28463  axtg5seg  28537  axtgupdim2  28543  axtgeucl  28544  brbtwn  28972  axlowdim  29034  axeuclidlem  29035  incistruhgr  29152  issubgr2  29345  wwlksnwwlksnon  29988  upgr4cycl4dv4e  30260  isnvlem  30685  csmdsymi  32409  br8d  32686  slmdlema  33285  constrconj  33902  constrllcllem  33909  constrcccllem  33911  constrcbvlem  33912  carsgmon  34471  sitgclg  34499  tgoldbachgt  34820  axtgupdim2ALTV  34825  bnj852  35077  bnj18eq1  35083  bnj938  35093  bnj983  35107  bnj1318  35181  bnj1326  35182  cvmlift3lem4  35516  cvmlift3  35522  br8  35950  br6  35951  br4  35952  brcolinear2  36252  colineardim1  36255  brfs  36273  fscgr  36274  btwnconn1lem7  36287  brsegle  36302  unblimceq0  36707  sdclem2  37943  sdclem1  37944  sdc  37945  fdc  37946  cdleme18d  40555  cdlemk35s  41197  cdlemk39s  41199  monotoddzz  43185  jm2.27  43250  mendlmod  43431  minregex2  43776  fiiuncl  45310  wessf1ornlem  45429  fmulcl  45827  fmuldfeqlem1  45828  fprodcncf  46144  dvmptfprodlem  46188  dvmptfprod  46189  dvnprodlem2  46191  stoweidlem6  46250  stoweidlem8  46252  stoweidlem31  46275  stoweidlem34  46278  stoweidlem43  46287  stoweidlem52  46296  fourierdlem41  46392  fourierdlem48  46398  fourierdlem49  46399  ovnsubaddlem1  46814  ichexmpl2  47716  9gbo  48020  11gbo  48021  lmod1  48738  cnelsubclem  49848