Theorem 3anbi1d 1439

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 1436	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  3581  vtocl3gaOLD  3583  axdc4uz  14021  wrdl3s3  14997  relexpindlem  15098  sqrtval  15272  sqreu  15395  coprmprod  16694  mreexexd  17692  iscatd2  17725  lmodprop2d  20938  neiptopnei  23155  hausnei  23351  isreg2  23400  regr1lem2  23763  ustval  24226  ustuqtop4  24268  axtgupdim2  28493  axtgeucl  28494  iscgra  28831  brbtwn  28928  ax5seg  28967  axlowdim  28990  axeuclidlem  28991  wlkonprop  29690  upgr2wlk  29700  upgrf1istrl  29735  elwspths2spth  29996  clwlkclwwlk  30030  clwwlknonel  30123  upgr4cycl4dv4e  30213  extwwlkfab  30380  nvi  30642  br8d  32629  xlt2addrd  32768  isslmd  33190  slmdlema  33191  tgoldbachgt  34656  axtgupdim2ALTV  34661  br8  35735  br6  35736  br4  35737  fvtransport  36013  brcolinear2  36039  colineardim1  36042  fscgr  36061  idinside  36065  brsegle  36089  poimirlem28  37634  caures  37746  iscringd  37984  oposlem  39163  cdleme18d  40277  jm2.27  42996  ichexmpl2  47394  ichnreuop  47396  9gbo  47698  11gbo  47699