Theorem 3anbi2d 1444

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

Syntax hints:   → wi 4   ↔ wb 196   ∧ w3a 1054

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 197  df-an 385  df-3an 1056

This theorem is referenced by:  vtocl3gaf  3306  offval22  7298  ereq2  7795  wrdl3s3  13751  mhmlem  17582  isdrngrd  18821  lmodlema  18916  mdetunilem9  20474  neiptoptop  20983  neiptopnei  20984  hausnei  21180  regr1lem2  21591  ustuqtop4  22095  utopsnneiplem  22098  axtg5seg  25409  axtgupdim2  25415  axtgeucl  25416  brbtwn  25824  axlowdim  25886  axeuclidlem  25887  incistruhgr  26019  issubgr2  26209  wwlksnwwlksnon  26878  wwlksnwwlksnonOLD  26880  upgr4cycl4dv4e  27163  isnvlem  27593  csmdsymi  29321  br8d  29548  slmdlema  29884  carsgmon  30504  sitgclg  30532  tgoldbachgt  30869  axtgupdim2OLD  30874  bnj852  31117  bnj18eq1  31123  bnj938  31133  bnj983  31147  bnj1318  31219  bnj1326  31220  cvmlift3lem4  31430  cvmlift3  31436  br8  31772  br6  31773  br4  31774  brcolinear2  32290  colineardim1  32293  brfs  32311  fscgr  32312  btwnconn1lem7  32325  brsegle  32340  unblimceq0  32623  sdclem2  33668  sdclem1  33669  sdc  33670  fdc  33671  cdleme18d  35900  cdlemk35s  36542  cdlemk39s  36544  monotoddzz  37825  jm2.27  37892  mendlmod  38080  fiiuncl  39548  wessf1ornlem  39685  fmulcl  40131  fmuldfeqlem1  40132  fprodcncf  40432  dvmptfprodlem  40477  dvmptfprod  40478  dvnprodlem2  40480  stoweidlem6  40541  stoweidlem8  40543  stoweidlem31  40566  stoweidlem34  40569  stoweidlem43  40578  stoweidlem52  40587  fourierdlem41  40683  fourierdlem48  40689  fourierdlem49  40690  ovnsubaddlem1  41105  9gbo  41987  11gbo  41988  lmod1  42606