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  3526  vtocl3gaOLD  3528  offval22  8032  ereq2  8646  brttrcl  9628  ttrclss  9635  ttrclselem2  9641  wrdl3s3  14918  mhmlem  19032  isdrngrd  20737  isdrngrdOLD  20739  lmodlema  20854  mdetunilem9  22598  neiptoptop  23109  neiptopnei  23110  hausnei  23306  regr1lem2  23718  ustuqtop4  24222  utopsnneiplem  24225  bdayfinbndlem1  28476  axtg5seg  28550  axtgupdim2  28556  axtgeucl  28557  brbtwn  28985  axlowdim  29047  axeuclidlem  29048  incistruhgr  29165  issubgr2  29358  wwlksnwwlksnon  30001  upgr4cycl4dv4e  30273  isnvlem  30699  csmdsymi  32423  br8d  32699  slmdlema  33282  constrconj  33908  constrllcllem  33915  constrcccllem  33917  constrcbvlem  33918  carsgmon  34477  sitgclg  34505  tgoldbachgt  34826  axtgupdim2ALTV  34831  bnj852  35082  bnj18eq1  35088  bnj938  35098  bnj983  35112  bnj1318  35186  bnj1326  35187  cvmlift3lem4  35523  cvmlift3  35529  br8  35957  br6  35958  br4  35959  brcolinear2  36259  colineardim1  36262  brfs  36280  fscgr  36281  btwnconn1lem7  36294  brsegle  36309  unblimceq0  36786  sdclem2  38080  sdclem1  38081  sdc  38082  fdc  38083  cdleme18d  40758  cdlemk35s  41400  cdlemk39s  41402  monotoddzz  43392  jm2.27  43457  mendlmod  43638  minregex2  43983  fiiuncl  45517  wessf1ornlem  45636  fmulcl  46032  fmuldfeqlem1  46033  fprodcncf  46349  dvmptfprodlem  46393  dvmptfprod  46394  dvnprodlem2  46396  stoweidlem6  46455  stoweidlem8  46457  stoweidlem31  46480  stoweidlem34  46483  stoweidlem43  46492  stoweidlem52  46501  fourierdlem41  46597  fourierdlem48  46603  fourierdlem49  46604  ovnsubaddlem1  47019  ichexmpl2  47945  9gbo  48265  11gbo  48266  lmod1  48983  cnelsubclem  50093