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

Syntax hints:   → wi 4   ↔ wb 205   ∧ 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 206  df-an 395  df-3an 1086

This theorem is referenced by:  vtocl3gafOLD  3563  vtocl3gaOLD  3565  axdc4uz  14004  wrdl3s3  14971  relexpindlem  15068  sqrtval  15242  sqreu  15365  coprmprod  16662  mreexexd  17661  iscatd2  17694  lmodprop2d  20900  neiptopnei  23127  hausnei  23323  isreg2  23372  regr1lem2  23735  ustval  24198  ustuqtop4  24240  axtgupdim2  28398  axtgeucl  28399  iscgra  28736  brbtwn  28833  ax5seg  28872  axlowdim  28895  axeuclidlem  28896  wlkonprop  29595  upgr2wlk  29605  upgrf1istrl  29640  elwspths2spth  29901  clwlkclwwlk  29935  clwwlknonel  30028  upgr4cycl4dv4e  30118  extwwlkfab  30285  nvi  30547  br8d  32530  xlt2addrd  32662  isslmd  33066  slmdlema  33067  tgoldbachgt  34509  axtgupdim2ALTV  34514  br8  35578  br6  35579  br4  35580  fvtransport  35856  brcolinear2  35882  colineardim1  35885  fscgr  35904  idinside  35908  brsegle  35932  poimirlem28  37349  caures  37461  iscringd  37699  oposlem  38880  cdleme18d  39994  jm2.27  42666  ichexmpl2  47042  ichnreuop  47044  9gbo  47346  11gbo  47347