Theorem 3anbi1d 1443

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 1440	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  3525  vtocl3gaOLD  3527  axdc4uz  13946  wrdl3s3  14924  relexpindlem  15025  sqrtval  15199  sqreu  15323  coprmprod  16630  mreexexd  17614  iscatd2  17647  lmodprop2d  20919  neiptopnei  23097  hausnei  23293  isreg2  23342  regr1lem2  23705  ustval  24168  ustuqtop4  24209  bdayfinbndcbv  28458  bdayfinbndlem1  28459  bdayfinbndlem2  28460  bdayfinbnd  28461  axtgupdim2  28539  axtgeucl  28540  iscgra  28877  brbtwn  28968  ax5seg  29007  axlowdim  29030  axeuclidlem  29031  wlkonprop  29725  upgr2wlk  29735  upgrf1istrl  29770  elwspths2spth  30038  clwlkclwwlk  30072  clwwlknonel  30165  upgr4cycl4dv4e  30255  extwwlkfab  30422  nvi  30685  br8d  32681  xlt2addrd  32832  isslmd  33263  slmdlema  33264  constrllcllem  33896  constrcbvlem  33899  tgoldbachgt  34807  axtgupdim2ALTV  34812  trssfir1om  35255  trssfir1omregs  35280  br8  35938  br6  35939  br4  35940  fvtransport  36214  brcolinear2  36240  colineardim1  36243  fscgr  36262  idinside  36266  brsegle  36290  poimirlem28  37969  caures  38081  iscringd  38319  oposlem  39628  cdleme18d  40741  jm2.27  43436  ichexmpl2  47930  ichnreuop  47932  9gbo  48250  11gbo  48251