Theorem 3anbi1d 1557

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

Syntax hints:   → wi 4   ↔ wb 197   ∧ w3a 1100

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 198  df-an 385  df-3an 1102

This theorem is referenced by:  vtocl3gaf  3468  axdc4uz  13003  wrdl3s3  13926  relexpindlem  14022  sqrtval  14196  sqreu  14319  coprmprod  15589  mreexexd  16509  iscatd2  16542  lmodprop2d  19125  neiptopnei  21147  hausnei  21343  isreg2  21392  regr1lem2  21754  ustval  22216  ustuqtop4  22258  axtgupdim2  25583  axtgeucl  25584  iscgra  25914  brbtwn  25992  ax5seg  26031  axlowdim  26054  axeuclidlem  26055  wlkonprop  26781  upgr2wlk  26791  upgrf1istrl  26827  elwspths2spth  27108  clwlkclwwlk  27144  clwwlknonel  27261  upgr4cycl4dv4e  27357  extwwlkfab  27530  nvi  27796  br8d  29746  xlt2addrd  29849  isslmd  30079  slmdlema  30080  tgoldbachgt  31065  axtgupdim2OLD  31070  br8  31966  br6  31967  br4  31968  fvtransport  32458  brcolinear2  32484  colineardim1  32487  fscgr  32506  idinside  32510  brsegle  32534  poimirlem28  33748  caures  33865  iscringd  34106  oposlem  34960  cdleme18d  36073  jm2.27  38073  9gbo  42234  11gbo  42235