Theorem 3anbi1d 1469

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 1466	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  14167  wrdl3s3  15158  relexpindlem  15259  sqrtval  15447  sqreu  15572  coprmprod  16880  mreexexd  17872  iscatd2  17905  lmodprop2d  21250  neiptopnei  23505  hausnei  23701  isreg2  23750  regr1lem2  24114  ustval  24577  ustuqtop4  24618  bdayfinbndcbv  28909  bdayfinbndlem1  28910  bdayfinbndlem2  28911  bdayfinbnd  28912  axtgupdim2  28990  axtgeucl  28991  iscgra  29373  brbtwn  29534  ax5seg  29573  axlowdim  29596  axeuclidlem  29597  wlkonprop  30294  upgr2wlk  30304  upgrf1istrl  30343  elwspths2spth  30616  clwlkclwwlk  30650  clwwlknonel  30743  upgr4cycl4dv4e  30843  extwwlkfab  31010  nvi  31273  br8d  33300  xlt2addrd  33447  isslmd  33862  slmdlema  33863  constrllcllem  34495  constrcbvlem  34498  tgoldbachgt  35403  axtgupdim2ALTV  35408  trssfihf  35860  trssfihfregs  35945  br8  36736  br6  36737  br4  36738  fvtransport  37012  brcolinear2  37038  colineardim1  37041  fscgr  37060  idinside  37064  brsegle  37088  poimirlem28  38834  caures  38960  iscringd  39198  oposlem  40505  cdleme18d  41618  jm2.27  44281  ichexmpl2  48825  ichnreuop  48827  9gbo  49145  11gbo  49146