Theorem 3anbi1d 1442

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 262	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃))
3	1, 2	3anbi12d 1439	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜏) ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  vtocl3gafOLD  3535  vtocl3gaOLD  3537  axdc4uz  13905  wrdl3s3  14883  relexpindlem  14984  sqrtval  15158  sqreu  15282  coprmprod  16586  mreexexd  17569  iscatd2  17602  lmodprop2d  20873  neiptopnei  23074  hausnei  23270  isreg2  23319  regr1lem2  23682  ustval  24145  ustuqtop4  24186  axtgupdim2  28492  axtgeucl  28493  iscgra  28830  brbtwn  28921  ax5seg  28960  axlowdim  28983  axeuclidlem  28984  wlkonprop  29679  upgr2wlk  29689  upgrf1istrl  29724  elwspths2spth  29992  clwlkclwwlk  30026  clwwlknonel  30119  upgr4cycl4dv4e  30209  extwwlkfab  30376  nvi  30638  br8d  32635  xlt2addrd  32788  isslmd  33233  slmdlema  33234  constrllcllem  33858  constrcbvlem  33861  tgoldbachgt  34769  axtgupdim2ALTV  34774  trssfir1om  35216  trssfir1omregs  35241  br8  35899  br6  35900  br4  35901  fvtransport  36175  brcolinear2  36201  colineardim1  36204  fscgr  36223  idinside  36227  brsegle  36251  poimirlem28  37788  caures  37900  iscringd  38138  oposlem  39381  cdleme18d  40494  jm2.27  43192  ichexmpl2  47658  ichnreuop  47660  9gbo  47962  11gbo  47963