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  3533  vtocl3gaOLD  3535  offval22  8018  ereq2  8630  brttrcl  9603  ttrclss  9610  ttrclselem2  9616  wrdl3s3  14869  mhmlem  18975  isdrngrd  20681  isdrngrdOLD  20683  lmodlema  20798  mdetunilem9  22535  neiptoptop  23046  neiptopnei  23047  hausnei  23243  regr1lem2  23655  ustuqtop4  24159  utopsnneiplem  24162  axtg5seg  28443  axtgupdim2  28449  axtgeucl  28450  brbtwn  28877  axlowdim  28939  axeuclidlem  28940  incistruhgr  29057  issubgr2  29250  wwlksnwwlksnon  29893  upgr4cycl4dv4e  30165  isnvlem  30590  csmdsymi  32314  br8d  32591  slmdlema  33172  constrconj  33758  constrllcllem  33765  constrcccllem  33767  constrcbvlem  33768  carsgmon  34327  sitgclg  34355  tgoldbachgt  34676  axtgupdim2ALTV  34681  bnj852  34933  bnj18eq1  34939  bnj938  34949  bnj983  34963  bnj1318  35037  bnj1326  35038  cvmlift3lem4  35366  cvmlift3  35372  br8  35800  br6  35801  br4  35802  brcolinear2  36100  colineardim1  36103  brfs  36121  fscgr  36122  btwnconn1lem7  36135  brsegle  36150  unblimceq0  36549  sdclem2  37790  sdclem1  37791  sdc  37792  fdc  37793  cdleme18d  40342  cdlemk35s  40984  cdlemk39s  40986  monotoddzz  42984  jm2.27  43049  mendlmod  43230  minregex2  43576  fiiuncl  45110  wessf1ornlem  45230  fmulcl  45629  fmuldfeqlem1  45630  fprodcncf  45946  dvmptfprodlem  45990  dvmptfprod  45991  dvnprodlem2  45993  stoweidlem6  46052  stoweidlem8  46054  stoweidlem31  46077  stoweidlem34  46080  stoweidlem43  46089  stoweidlem52  46098  fourierdlem41  46194  fourierdlem48  46200  fourierdlem49  46201  ovnsubaddlem1  46616  ichexmpl2  47509  9gbo  47813  11gbo  47814  lmod1  48532  cnelsubclem  49643