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  14048  wrdl3s3  15035  relexpindlem  15136  sqrtval  15324  sqreu  15448  coprmprod  16751  mreexexd  17736  iscatd2  17769  lmodprop2d  21108  neiptopnei  23357  hausnei  23553  isreg2  23602  regr1lem2  23966  ustval  24429  ustuqtop4  24470  bdayfinbndcbv  28731  bdayfinbndlem1  28732  bdayfinbndlem2  28733  bdayfinbnd  28734  axtgupdim2  28812  axtgeucl  28813  iscgra  29195  brbtwn  29356  ax5seg  29395  axlowdim  29418  axeuclidlem  29419  wlkonprop  30116  upgr2wlk  30126  upgrf1istrl  30165  elwspths2spth  30438  clwlkclwwlk  30472  clwwlknonel  30565  upgr4cycl4dv4e  30665  extwwlkfab  30832  nvi  31095  br8d  33081  xlt2addrd  33230  isslmd  33642  slmdlema  33643  constrllcllem  34262  constrcbvlem  34265  tgoldbachgt  35171  axtgupdim2ALTV  35176  trssfir1om  35621  trssfir1omregs  35662  br8  36335  br6  36336  br4  36337  fvtransport  36612  brcolinear2  36638  colineardim1  36641  fscgr  36660  idinside  36664  brsegle  36688  poimirlem28  38397  caures  38510  iscringd  38748  oposlem  40055  cdleme18d  41168  jm2.27  43849  ichexmpl2  48370  ichnreuop  48372  9gbo  48690  11gbo  48691