Theorem 3anbi2d 1442

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1086

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 1088

This theorem is referenced by:  vtocl3gafOLD  3565  vtocl3gaOLD  3567  offval22  8095  ereq2  8735  brttrcl  9735  ttrclss  9742  ttrclselem2  9748  wrdl3s3  14983  mhmlem  19049  isdrngrd  20734  isdrngrdOLD  20736  lmodlema  20831  mdetunilem9  22574  neiptoptop  23085  neiptopnei  23086  hausnei  23282  regr1lem2  23694  ustuqtop4  24199  utopsnneiplem  24202  axtg5seg  28409  axtgupdim2  28415  axtgeucl  28416  brbtwn  28844  axlowdim  28906  axeuclidlem  28907  incistruhgr  29024  issubgr2  29217  wwlksnwwlksnon  29863  upgr4cycl4dv4e  30132  isnvlem  30557  csmdsymi  32281  br8d  32557  slmdlema  33148  constrconj  33725  constrllcllem  33732  constrcccllem  33734  constrcbvlem  33735  carsgmon  34275  sitgclg  34303  tgoldbachgt  34637  axtgupdim2ALTV  34642  bnj852  34894  bnj18eq1  34900  bnj938  34910  bnj983  34924  bnj1318  34998  bnj1326  34999  cvmlift3lem4  35286  cvmlift3  35292  br8  35715  br6  35716  br4  35717  brcolinear2  36018  colineardim1  36021  brfs  36039  fscgr  36040  btwnconn1lem7  36053  brsegle  36068  unblimceq0  36467  sdclem2  37708  sdclem1  37709  sdc  37710  fdc  37711  cdleme18d  40256  cdlemk35s  40898  cdlemk39s  40900  monotoddzz  42918  jm2.27  42983  mendlmod  43164  minregex2  43510  fiiuncl  45027  wessf1ornlem  45147  fmulcl  45553  fmuldfeqlem1  45554  fprodcncf  45872  dvmptfprodlem  45916  dvmptfprod  45917  dvnprodlem2  45919  stoweidlem6  45978  stoweidlem8  45980  stoweidlem31  46003  stoweidlem34  46006  stoweidlem43  46015  stoweidlem52  46024  fourierdlem41  46120  fourierdlem48  46126  fourierdlem49  46127  ovnsubaddlem1  46542  ichexmpl2  47415  9gbo  47719  11gbo  47720  lmod1  48367