Theorem 3anbi2d 1443

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 1439	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  3535  vtocl3gaOLD  3537  offval22  8028  ereq2  8641  brttrcl  9620  ttrclss  9627  ttrclselem2  9633  wrdl3s3  14883  mhmlem  18990  isdrngrd  20697  isdrngrdOLD  20699  lmodlema  20814  mdetunilem9  22562  neiptoptop  23073  neiptopnei  23074  hausnei  23270  regr1lem2  23682  ustuqtop4  24186  utopsnneiplem  24189  axtg5seg  28486  axtgupdim2  28492  axtgeucl  28493  brbtwn  28921  axlowdim  28983  axeuclidlem  28984  incistruhgr  29101  issubgr2  29294  wwlksnwwlksnon  29937  upgr4cycl4dv4e  30209  isnvlem  30634  csmdsymi  32358  br8d  32635  slmdlema  33234  constrconj  33851  constrllcllem  33858  constrcccllem  33860  constrcbvlem  33861  carsgmon  34420  sitgclg  34448  tgoldbachgt  34769  axtgupdim2ALTV  34774  bnj852  35026  bnj18eq1  35032  bnj938  35042  bnj983  35056  bnj1318  35130  bnj1326  35131  cvmlift3lem4  35465  cvmlift3  35471  br8  35899  br6  35900  br4  35901  brcolinear2  36201  colineardim1  36204  brfs  36222  fscgr  36223  btwnconn1lem7  36236  brsegle  36251  unblimceq0  36650  sdclem2  37882  sdclem1  37883  sdc  37884  fdc  37885  cdleme18d  40494  cdlemk35s  41136  cdlemk39s  41138  monotoddzz  43127  jm2.27  43192  mendlmod  43373  minregex2  43718  fiiuncl  45252  wessf1ornlem  45371  fmulcl  45769  fmuldfeqlem1  45770  fprodcncf  46086  dvmptfprodlem  46130  dvmptfprod  46131  dvnprodlem2  46133  stoweidlem6  46192  stoweidlem8  46194  stoweidlem31  46217  stoweidlem34  46220  stoweidlem43  46229  stoweidlem52  46238  fourierdlem41  46334  fourierdlem48  46340  fourierdlem49  46341  ovnsubaddlem1  46756  ichexmpl2  47658  9gbo  47962  11gbo  47963  lmod1  48680  cnelsubclem  49790