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 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜏) ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  axdc4uz  14134  wrdl3s3  15124  relexpindlem  15225  sqrtval  15413  sqreu  15537  coprmprod  16845  mreexexd  17831  iscatd2  17864  lmodprop2d  21208  neiptopnei  23459  hausnei  23655  isreg2  23704  regr1lem2  24068  ustval  24531  ustuqtop4  24572  bdayfinbndcbv  28861  bdayfinbndlem1  28862  bdayfinbndlem2  28863  bdayfinbnd  28864  axtgupdim2  28942  axtgeucl  28943  iscgra  29325  brbtwn  29486  ax5seg  29525  axlowdim  29548  axeuclidlem  29549  wlkonprop  30246  upgr2wlk  30256  upgrf1istrl  30295  elwspths2spth  30568  clwlkclwwlk  30602  clwwlknonel  30695  upgr4cycl4dv4e  30795  extwwlkfab  30962  nvi  31225  br8d  33253  xlt2addrd  33401  isslmd  33813  slmdlema  33814  constrllcllem  34434  constrcbvlem  34437  tgoldbachgt  35342  axtgupdim2ALTV  35347  trssfir1om  35795  trssfir1omregs  35872  br8  36645  br6  36646  br4  36647  fvtransport  36921  brcolinear2  36947  colineardim1  36950  fscgr  36969  idinside  36973  brsegle  36997  poimirlem28  38703  caures  38831  iscringd  39069  oposlem  40376  cdleme18d  41489  jm2.27  44152  ichexmpl2  48688  ichnreuop  48690  9gbo  49008  11gbo  49009