Theorem 3anbi1d 1440

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1087

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 397  df-3an 1089

This theorem is referenced by:  vtocl3gaf  3568  vtocl3ga  3569  axdc4uz  13953  wrdl3s3  14917  relexpindlem  15014  sqrtval  15188  sqreu  15311  coprmprod  16602  mreexexd  17596  iscatd2  17629  lmodprop2d  20678  neiptopnei  22856  hausnei  23052  isreg2  23101  regr1lem2  23464  ustval  23927  ustuqtop4  23969  axtgupdim2  27977  axtgeucl  27978  iscgra  28315  brbtwn  28412  ax5seg  28451  axlowdim  28474  axeuclidlem  28475  wlkonprop  29170  upgr2wlk  29180  upgrf1istrl  29215  elwspths2spth  29476  clwlkclwwlk  29510  clwwlknonel  29603  upgr4cycl4dv4e  29693  extwwlkfab  29860  nvi  30122  br8d  32094  xlt2addrd  32226  isslmd  32605  slmdlema  32606  tgoldbachgt  33961  axtgupdim2ALTV  33966  br8  35018  br6  35019  br4  35020  fvtransport  35296  brcolinear2  35322  colineardim1  35325  fscgr  35344  idinside  35348  brsegle  35372  poimirlem28  36819  caures  36931  iscringd  37169  oposlem  38355  cdleme18d  39469  jm2.27  42049  ichexmpl2  46437  ichnreuop  46439  9gbo  46741  11gbo  46742