Theorem 3anbi1d 1466

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  axdc4uz  14019  wrdl3s3  14998  relexpindlem  15099  sqrtval  15287  sqreu  15411  coprmprod  16718  mreexexd  17703  iscatd2  17736  lmodprop2d  21022  neiptopnei  23257  hausnei  23453  isreg2  23502  regr1lem2  23865  ustval  24328  ustuqtop4  24369  bdayfinbndcbv  28624  bdayfinbndlem1  28625  bdayfinbndlem2  28626  bdayfinbnd  28627  axtgupdim2  28705  axtgeucl  28706  iscgra  29076  brbtwn  29189  ax5seg  29228  axlowdim  29251  axeuclidlem  29252  wlkonprop  29946  upgr2wlk  29956  upgrf1istrl  29991  elwspths2spth  30259  clwlkclwwlk  30293  clwwlknonel  30386  upgr4cycl4dv4e  30476  extwwlkfab  30643  nvi  30906  br8d  32893  xlt2addrd  33044  isslmd  33462  slmdlema  33463  constrllcllem  34086  constrcbvlem  34089  tgoldbachgt  34994  axtgupdim2ALTV  34999  trssfir1om  35446  trssfir1omregs  35471  br8  36146  br6  36147  br4  36148  fvtransport  36422  brcolinear2  36448  colineardim1  36451  fscgr  36470  idinside  36474  brsegle  36498  poimirlem28  38186  caures  38298  iscringd  38536  oposlem  39845  cdleme18d  40958  jm2.27  43626  ichexmpl2  48107  ichnreuop  48109  9gbo  48427  11gbo  48428