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  14038  wrdl3s3  15023  relexpindlem  15124  sqrtval  15312  sqreu  15436  coprmprod  16741  mreexexd  17726  iscatd2  17759  lmodprop2d  21095  neiptopnei  23339  hausnei  23535  isreg2  23584  regr1lem2  23948  ustval  24411  ustuqtop4  24452  bdayfinbndcbv  28710  bdayfinbndlem1  28711  bdayfinbndlem2  28712  bdayfinbnd  28713  axtgupdim2  28791  axtgeucl  28792  iscgra  29171  brbtwn  29304  ax5seg  29343  axlowdim  29366  axeuclidlem  29367  wlkonprop  30064  upgr2wlk  30074  upgrf1istrl  30113  elwspths2spth  30386  clwlkclwwlk  30420  clwwlknonel  30513  upgr4cycl4dv4e  30607  extwwlkfab  30774  nvi  31037  br8d  33024  xlt2addrd  33174  isslmd  33586  slmdlema  33587  constrllcllem  34206  constrcbvlem  34209  tgoldbachgt  35115  axtgupdim2ALTV  35120  trssfir1om  35565  trssfir1omregs  35606  br8  36285  br6  36286  br4  36287  fvtransport  36561  brcolinear2  36587  colineardim1  36590  fscgr  36609  idinside  36613  brsegle  36637  poimirlem28  38356  caures  38469  iscringd  38707  oposlem  40014  cdleme18d  41127  jm2.27  43793  ichexmpl2  48277  ichnreuop  48279  9gbo  48597  11gbo  48598