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  3545  vtocl3gaOLD  3547  offval22  8044  ereq2  8656  brttrcl  9642  ttrclss  9649  ttrclselem2  9655  wrdl3s3  14904  mhmlem  18976  isdrngrd  20686  isdrngrdOLD  20688  lmodlema  20803  mdetunilem9  22540  neiptoptop  23051  neiptopnei  23052  hausnei  23248  regr1lem2  23660  ustuqtop4  24165  utopsnneiplem  24168  axtg5seg  28445  axtgupdim2  28451  axtgeucl  28452  brbtwn  28879  axlowdim  28941  axeuclidlem  28942  incistruhgr  29059  issubgr2  29252  wwlksnwwlksnon  29895  upgr4cycl4dv4e  30164  isnvlem  30589  csmdsymi  32313  br8d  32588  slmdlema  33172  constrconj  33728  constrllcllem  33735  constrcccllem  33737  constrcbvlem  33738  carsgmon  34298  sitgclg  34326  tgoldbachgt  34647  axtgupdim2ALTV  34652  bnj852  34904  bnj18eq1  34910  bnj938  34920  bnj983  34934  bnj1318  35008  bnj1326  35009  cvmlift3lem4  35302  cvmlift3  35308  br8  35736  br6  35737  br4  35738  brcolinear2  36039  colineardim1  36042  brfs  36060  fscgr  36061  btwnconn1lem7  36074  brsegle  36089  unblimceq0  36488  sdclem2  37729  sdclem1  37730  sdc  37731  fdc  37732  cdleme18d  40282  cdlemk35s  40924  cdlemk39s  40926  monotoddzz  42925  jm2.27  42990  mendlmod  43171  minregex2  43517  fiiuncl  45052  wessf1ornlem  45172  fmulcl  45572  fmuldfeqlem1  45573  fprodcncf  45891  dvmptfprodlem  45935  dvmptfprod  45936  dvnprodlem2  45938  stoweidlem6  45997  stoweidlem8  45999  stoweidlem31  46022  stoweidlem34  46025  stoweidlem43  46034  stoweidlem52  46043  fourierdlem41  46139  fourierdlem48  46145  fourierdlem49  46146  ovnsubaddlem1  46561  ichexmpl2  47464  9gbo  47768  11gbo  47769  lmod1  48474  cnelsubclem  49585