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

This theorem is referenced by:  vtocl3gafOLD  3582  vtocl3gaOLD  3584  axdc4uz  14025  wrdl3s3  15001  relexpindlem  15102  sqrtval  15276  sqreu  15399  coprmprod  16698  mreexexd  17691  iscatd2  17724  lmodprop2d  20922  neiptopnei  23140  hausnei  23336  isreg2  23385  regr1lem2  23748  ustval  24211  ustuqtop4  24253  axtgupdim2  28479  axtgeucl  28480  iscgra  28817  brbtwn  28914  ax5seg  28953  axlowdim  28976  axeuclidlem  28977  wlkonprop  29676  upgr2wlk  29686  upgrf1istrl  29721  elwspths2spth  29987  clwlkclwwlk  30021  clwwlknonel  30114  upgr4cycl4dv4e  30204  extwwlkfab  30371  nvi  30633  br8d  32622  xlt2addrd  32762  isslmd  33208  slmdlema  33209  tgoldbachgt  34678  axtgupdim2ALTV  34683  br8  35756  br6  35757  br4  35758  fvtransport  36033  brcolinear2  36059  colineardim1  36062  fscgr  36081  idinside  36085  brsegle  36109  poimirlem28  37655  caures  37767  iscringd  38005  oposlem  39183  cdleme18d  40297  jm2.27  43020  ichexmpl2  47457  ichnreuop  47459  9gbo  47761  11gbo  47762