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

Syntax hints:   → wi 4   ↔ wb 196   ∧ w3a 1054

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 197  df-an 385  df-3an 1056

This theorem is referenced by:  vtocl3gaf  3306  axdc4uz  12823  wrdl3s3  13751  relexpindlem  13847  sqrtval  14021  sqreu  14144  coprmprod  15422  mreexexd  16355  mreexexdOLD  16356  iscatd2  16389  lmodprop2d  18973  neiptopnei  20984  hausnei  21180  isreg2  21229  regr1lem2  21591  ustval  22053  ustuqtop4  22095  axtgupdim2  25415  axtgeucl  25416  iscgra  25746  brbtwn  25824  ax5seg  25863  axlowdim  25886  axeuclidlem  25887  wlkonprop  26610  upgr2wlk  26620  upgrf1istrl  26656  elwspths2spth  26934  clwlkclwwlk  26968  clwwlknonel  27070  upgr4cycl4dv4e  27163  extwwlkfab  27342  nvi  27597  br8d  29548  xlt2addrd  29651  isslmd  29883  slmdlema  29884  tgoldbachgt  30869  axtgupdim2OLD  30874  br8  31772  br6  31773  br4  31774  fvtransport  32264  brcolinear2  32290  colineardim1  32293  fscgr  32312  idinside  32316  brsegle  32340  poimirlem28  33567  caures  33686  iscringd  33927  oposlem  34787  cdleme18d  35900  jm2.27  37892  9gbo  41987  11gbo  41988