Theorem 3anbi1d 1437

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

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

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 400  df-3an 1086

This theorem is referenced by:  vtocl3gaf  3525  axdc4uz  13347  wrdl3s3  14317  relexpindlem  14414  sqrtval  14588  sqreu  14712  coprmprod  15995  mreexexd  16911  iscatd2  16944  lmodprop2d  19689  neiptopnei  21737  hausnei  21933  isreg2  21982  regr1lem2  22345  ustval  22808  ustuqtop4  22850  axtgupdim2  26265  axtgeucl  26266  iscgra  26603  brbtwn  26693  ax5seg  26732  axlowdim  26755  axeuclidlem  26756  wlkonprop  27448  upgr2wlk  27458  upgrf1istrl  27493  elwspths2spth  27753  clwlkclwwlk  27787  clwwlknonel  27880  upgr4cycl4dv4e  27970  extwwlkfab  28137  nvi  28397  br8d  30374  xlt2addrd  30508  isslmd  30880  slmdlema  30881  tgoldbachgt  32044  axtgupdim2ALTV  32049  br8  33105  br6  33106  br4  33107  fvtransport  33606  brcolinear2  33632  colineardim1  33635  fscgr  33654  idinside  33658  brsegle  33682  poimirlem28  35085  caures  35198  iscringd  35436  oposlem  36478  cdleme18d  37591  jm2.27  39949  ichexmpl2  43987  ichnreuop  43989  9gbo  44292  11gbo  44293