Theorem 3anbi1d 1468

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 265	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃))
3	1, 2	3anbi12d 1465	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜏) ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  axdc4uz  14016  wrdl3s3  14995  relexpindlem  15096  sqrtval  15284  sqreu  15408  coprmprod  16714  mreexexd  17699  iscatd2  17732  lmodprop2d  21045  neiptopnei  23289  hausnei  23485  isreg2  23534  regr1lem2  23897  ustval  24360  ustuqtop4  24401  bdayfinbndcbv  28659  bdayfinbndlem1  28660  bdayfinbndlem2  28661  bdayfinbnd  28662  axtgupdim2  28740  axtgeucl  28741  iscgra  29120  brbtwn  29249  ax5seg  29288  axlowdim  29311  axeuclidlem  29312  wlkonprop  30006  upgr2wlk  30016  upgrf1istrl  30051  elwspths2spth  30319  clwlkclwwlk  30353  clwwlknonel  30446  upgr4cycl4dv4e  30536  extwwlkfab  30703  nvi  30966  br8d  32953  xlt2addrd  33104  isslmd  33522  slmdlema  33523  constrllcllem  34142  constrcbvlem  34145  tgoldbachgt  35050  axtgupdim2ALTV  35055  trssfir1om  35507  trssfir1omregs  35549  br8  36248  br6  36249  br4  36250  fvtransport  36524  brcolinear2  36550  colineardim1  36553  fscgr  36572  idinside  36576  brsegle  36600  poimirlem28  38299  caures  38411  iscringd  38649  oposlem  39956  cdleme18d  41069  jm2.27  43735  ichexmpl2  48219  ichnreuop  48221  9gbo  48539  11gbo  48540