Theorem 3anbi1d 1395

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

Syntax hints:   → wi 4   ↔ wb 195   ∧ w3a 1031

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 196  df-an 385  df-3an 1033

This theorem is referenced by:  vtocl3gaf  3248  axdc4uz  12645  wrdl3s3  13553  relexpindlem  13651  sqrtval  13825  sqreu  13948  coprmprod  15213  mreexexd  16131  mreexexdOLD  16132  iscatd2  16165  lmodprop2d  18748  neiptopnei  20746  hausnei  20942  isreg2  20991  regr1lem2  21353  ustval  21816  ustuqtop4  21858  axtgupdim2  25170  axtgeucl  25171  iscgra  25501  brbtwn  25579  ax5seg  25618  axlowdim  25641  axeuclidlem  25642  wlkon  26061  wlkonprop  26063  istrl2  26068  is2wlk  26095  pths  26096  is2wlkonot  26390  is2spthonot  26391  el2wlkonot  26396  el2spthonot  26397  el2spthonot0  26398  2wlkonot3v  26402  2spthonot3v  26403  extwwlkfab  26617  nvi  26853  br8d  28802  xlt2addrd  28913  isslmd  29086  slmdlema  29087  axtgupdim2OLD  29999  br8  30899  br6  30900  br4  30901  fvtransport  31309  brcolinear2  31335  colineardim1  31338  fscgr  31357  idinside  31361  brsegle  31385  poimirlem28  32607  caures  32726  iscringd  32967  oposlem  33487  cdleme18d  34600  jm2.27  36593  9gboa  40196  11gboa  40197  wlkOnprop  40866  upgr2wlk  40876  upgrf1istrl  40911  elwspths2spth  41171  clwlkclwwlk  41211  upgr4cycl4dv4e  41352  av-extwwlkfab  41520