Theorem 3anbi1d 1439

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  vtocl3gaf  3517  vtocl3ga  3518  axdc4uz  13713  wrdl3s3  14686  relexpindlem  14783  sqrtval  14957  sqreu  15081  coprmprod  16375  mreexexd  17366  iscatd2  17399  lmodprop2d  20194  neiptopnei  22292  hausnei  22488  isreg2  22537  regr1lem2  22900  ustval  23363  ustuqtop4  23405  axtgupdim2  26841  axtgeucl  26842  iscgra  27179  brbtwn  27276  ax5seg  27315  axlowdim  27338  axeuclidlem  27339  wlkonprop  28035  upgr2wlk  28045  upgrf1istrl  28080  elwspths2spth  28341  clwlkclwwlk  28375  clwwlknonel  28468  upgr4cycl4dv4e  28558  extwwlkfab  28725  nvi  28985  br8d  30959  xlt2addrd  31090  isslmd  31464  slmdlema  31465  tgoldbachgt  32652  axtgupdim2ALTV  32657  br8  33732  br6  33733  br4  33734  fvtransport  34343  brcolinear2  34369  colineardim1  34372  fscgr  34391  idinside  34395  brsegle  34419  poimirlem28  35814  caures  35927  iscringd  36165  oposlem  37203  cdleme18d  38316  jm2.27  40837  ichexmpl2  44933  ichnreuop  44935  9gbo  45237  11gbo  45238