Theorem 3anbi1d 1448

Description: Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)

Hypothesis

Ref	Expression
3anbi1d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
3anbi1d	⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜏) ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))

Proof of Theorem 3anbi1d

Step	Hyp	Ref	Expression
1		3anbi1d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		biidd 263	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃))
3	1, 2	3anbi12d 1445	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜏) ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 207   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  axdc4uz  13937  wrdl3s3  14915  relexpindlem  15016  sqrtval  15190  sqreu  15314  coprmprod  16621  mreexexd  17605  iscatd2  17638  lmodprop2d  20914  neiptopnei  23115  hausnei  23311  isreg2  23360  regr1lem2  23723  ustval  24186  ustuqtop4  24227  bdayfinbndcbv  28476  bdayfinbndlem1  28477  bdayfinbndlem2  28478  bdayfinbnd  28479  axtgupdim2  28557  axtgeucl  28558  iscgra  28895  brbtwn  28986  ax5seg  29025  axlowdim  29048  axeuclidlem  29049  wlkonprop  29743  upgr2wlk  29753  upgrf1istrl  29788  elwspths2spth  30056  clwlkclwwlk  30090  clwwlknonel  30183  upgr4cycl4dv4e  30273  extwwlkfab  30440  nvi  30703  br8d  32700  xlt2addrd  32851  isslmd  33283  slmdlema  33284  constrllcllem  33936  constrcbvlem  33939  tgoldbachgt  34847  axtgupdim2ALTV  34852  trssfir1om  35292  trssfir1omregs  35317  br8  35984  br6  35985  br4  35986  fvtransport  36260  brcolinear2  36286  colineardim1  36289  fscgr  36308  idinside  36312  brsegle  36336  poimirlem28  38015  caures  38127  iscringd  38365  oposlem  39674  cdleme18d  40787  jm2.27  43453  ichexmpl2  47945  ichnreuop  47947  9gbo  48265  11gbo  48266