Theorem 3anbi2d 1433

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ w3a 1080

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

This theorem is referenced by:  vtocl3gaf  3520  offval22  7644  ereq2  8152  wrdl3s3  14165  mhmlem  17981  isdrngrd  19223  lmodlema  19334  mdetunilem9  20918  neiptoptop  21428  neiptopnei  21429  hausnei  21625  regr1lem2  22037  ustuqtop4  22541  utopsnneiplem  22544  axtg5seg  25938  axtgupdim2  25944  axtgeucl  25945  brbtwn  26373  axlowdim  26435  axeuclidlem  26436  incistruhgr  26552  issubgr2  26742  wwlksnwwlksnon  27386  upgr4cycl4dv4e  27656  isnvlem  28083  csmdsymi  29807  br8d  30056  slmdlema  30474  carsgmon  31194  sitgclg  31222  tgoldbachgt  31556  axtgupdim2ALTV  31561  bnj852  31814  bnj18eq1  31820  bnj938  31830  bnj983  31844  bnj1318  31916  bnj1326  31917  cvmlift3lem4  32184  cvmlift3  32190  br8  32607  br6  32608  br4  32609  brcolinear2  33135  colineardim1  33138  brfs  33156  fscgr  33157  btwnconn1lem7  33170  brsegle  33185  unblimceq0  33462  sdclem2  34575  sdclem1  34576  sdc  34577  fdc  34578  cdleme18d  36988  cdlemk35s  37630  cdlemk39s  37632  monotoddzz  39051  jm2.27  39116  mendlmod  39304  fiiuncl  40892  wessf1ornlem  41011  fmulcl  41430  fmuldfeqlem1  41431  fprodcncf  41752  dvmptfprodlem  41797  dvmptfprod  41798  dvnprodlem2  41800  stoweidlem6  41860  stoweidlem8  41862  stoweidlem31  41885  stoweidlem34  41888  stoweidlem43  41897  stoweidlem52  41906  fourierdlem41  42002  fourierdlem48  42008  fourierdlem49  42009  ovnsubaddlem1  42421  ichexmpl2  43141  9gbo  43448  11gbo  43449  lmod1  44054