Theorem 3anbi2d 1439

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

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

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

This theorem is referenced by:  vtocl3gaf  3506  vtocl3ga  3507  offval22  7899  ereq2  8464  wrdl3s3  14605  mhmlem  18610  isdrngrd  19932  lmodlema  20043  mdetunilem9  21677  neiptoptop  22190  neiptopnei  22191  hausnei  22387  regr1lem2  22799  ustuqtop4  23304  utopsnneiplem  23307  axtg5seg  26730  axtgupdim2  26736  axtgeucl  26737  brbtwn  27170  axlowdim  27232  axeuclidlem  27233  incistruhgr  27352  issubgr2  27542  wwlksnwwlksnon  28181  upgr4cycl4dv4e  28450  isnvlem  28873  csmdsymi  30597  br8d  30851  slmdlema  31358  carsgmon  32181  sitgclg  32209  tgoldbachgt  32543  axtgupdim2ALTV  32548  bnj852  32801  bnj18eq1  32807  bnj938  32817  bnj983  32831  bnj1318  32905  bnj1326  32906  cvmlift3lem4  33184  cvmlift3  33190  br8  33629  br6  33630  br4  33631  brttrcl  33699  ttrclss  33706  ttrclselem2  33712  brcolinear2  34287  colineardim1  34290  brfs  34308  fscgr  34309  btwnconn1lem7  34322  brsegle  34337  unblimceq0  34614  sdclem2  35827  sdclem1  35828  sdc  35829  fdc  35830  cdleme18d  38236  cdlemk35s  38878  cdlemk39s  38880  monotoddzz  40681  jm2.27  40746  mendlmod  40934  fiiuncl  42502  wessf1ornlem  42611  fmulcl  43012  fmuldfeqlem1  43013  fprodcncf  43331  dvmptfprodlem  43375  dvmptfprod  43376  dvnprodlem2  43378  stoweidlem6  43437  stoweidlem8  43439  stoweidlem31  43462  stoweidlem34  43465  stoweidlem43  43474  stoweidlem52  43483  fourierdlem41  43579  fourierdlem48  43585  fourierdlem49  43586  ovnsubaddlem1  43998  ichexmpl2  44810  9gbo  45114  11gbo  45115  lmod1  45721