Theorem 3anbi2d 1441

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

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

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

This theorem is referenced by:  vtocl3gaf  3538  vtocl3ga  3539  offval22  8025  ereq2  8663  brttrcl  9658  ttrclss  9665  ttrclselem2  9671  wrdl3s3  14863  mhmlem  18881  isdrngrd  20256  isdrngrdOLD  20258  lmodlema  20383  mdetunilem9  22006  neiptoptop  22519  neiptopnei  22520  hausnei  22716  regr1lem2  23128  ustuqtop4  23633  utopsnneiplem  23636  axtg5seg  27470  axtgupdim2  27476  axtgeucl  27477  brbtwn  27911  axlowdim  27973  axeuclidlem  27974  incistruhgr  28093  issubgr2  28283  wwlksnwwlksnon  28923  upgr4cycl4dv4e  29192  isnvlem  29615  csmdsymi  31339  br8d  31596  slmdlema  32108  carsgmon  33003  sitgclg  33031  tgoldbachgt  33365  axtgupdim2ALTV  33370  bnj852  33622  bnj18eq1  33628  bnj938  33638  bnj983  33652  bnj1318  33726  bnj1326  33727  cvmlift3lem4  34003  cvmlift3  34009  br8  34415  br6  34416  br4  34417  brcolinear2  34719  colineardim1  34722  brfs  34740  fscgr  34741  btwnconn1lem7  34754  brsegle  34769  unblimceq0  35046  sdclem2  36274  sdclem1  36275  sdc  36276  fdc  36277  cdleme18d  38831  cdlemk35s  39473  cdlemk39s  39475  monotoddzz  41325  jm2.27  41390  mendlmod  41578  minregex2  41929  fiiuncl  43395  wessf1ornlem  43525  fmulcl  43942  fmuldfeqlem1  43943  fprodcncf  44261  dvmptfprodlem  44305  dvmptfprod  44306  dvnprodlem2  44308  stoweidlem6  44367  stoweidlem8  44369  stoweidlem31  44392  stoweidlem34  44395  stoweidlem43  44404  stoweidlem52  44413  fourierdlem41  44509  fourierdlem48  44515  fourierdlem49  44516  ovnsubaddlem1  44931  ichexmpl2  45782  9gbo  46086  11gbo  46087  lmod1  46693