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

Syntax hints:   → wi 4   ↔ wb 206   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  vtocl3gafOLD  3525  vtocl3gaOLD  3527  offval22  8038  ereq2  8652  brttrcl  9634  ttrclss  9641  ttrclselem2  9647  wrdl3s3  14924  mhmlem  19038  isdrngrd  20743  isdrngrdOLD  20745  lmodlema  20860  mdetunilem9  22585  neiptoptop  23096  neiptopnei  23097  hausnei  23293  regr1lem2  23705  ustuqtop4  24209  utopsnneiplem  24212  bdayfinbndlem1  28459  axtg5seg  28533  axtgupdim2  28539  axtgeucl  28540  brbtwn  28968  axlowdim  29030  axeuclidlem  29031  incistruhgr  29148  issubgr2  29341  wwlksnwwlksnon  29983  upgr4cycl4dv4e  30255  isnvlem  30681  csmdsymi  32405  br8d  32681  slmdlema  33264  constrconj  33889  constrllcllem  33896  constrcccllem  33898  constrcbvlem  33899  carsgmon  34458  sitgclg  34486  tgoldbachgt  34807  axtgupdim2ALTV  34812  bnj852  35063  bnj18eq1  35069  bnj938  35079  bnj983  35093  bnj1318  35167  bnj1326  35168  cvmlift3lem4  35504  cvmlift3  35510  br8  35938  br6  35939  br4  35940  brcolinear2  36240  colineardim1  36243  brfs  36261  fscgr  36262  btwnconn1lem7  36275  brsegle  36290  unblimceq0  36767  sdclem2  38063  sdclem1  38064  sdc  38065  fdc  38066  cdleme18d  40741  cdlemk35s  41383  cdlemk39s  41385  monotoddzz  43371  jm2.27  43436  mendlmod  43617  minregex2  43962  fiiuncl  45496  wessf1ornlem  45615  fmulcl  46011  fmuldfeqlem1  46012  fprodcncf  46328  dvmptfprodlem  46372  dvmptfprod  46373  dvnprodlem2  46375  stoweidlem6  46434  stoweidlem8  46436  stoweidlem31  46459  stoweidlem34  46462  stoweidlem43  46471  stoweidlem52  46480  fourierdlem41  46576  fourierdlem48  46582  fourierdlem49  46583  ovnsubaddlem1  46998  ichexmpl2  47930  9gbo  48250  11gbo  48251  lmod1  48968  cnelsubclem  50078