Theorem 3anbi1d 1442

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 1439	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜏) ↔ (𝜒 ∧ 𝜃 ∧ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  vtocl3gafOLD  3533  vtocl3gaOLD  3535  axdc4uz  13891  wrdl3s3  14869  relexpindlem  14970  sqrtval  15144  sqreu  15268  coprmprod  16572  mreexexd  17554  iscatd2  17587  lmodprop2d  20857  neiptopnei  23047  hausnei  23243  isreg2  23292  regr1lem2  23655  ustval  24118  ustuqtop4  24159  axtgupdim2  28449  axtgeucl  28450  iscgra  28787  brbtwn  28877  ax5seg  28916  axlowdim  28939  axeuclidlem  28940  wlkonprop  29635  upgr2wlk  29645  upgrf1istrl  29680  elwspths2spth  29948  clwlkclwwlk  29982  clwwlknonel  30075  upgr4cycl4dv4e  30165  extwwlkfab  30332  nvi  30594  br8d  32591  xlt2addrd  32742  isslmd  33171  slmdlema  33172  constrllcllem  33765  constrcbvlem  33768  tgoldbachgt  34676  axtgupdim2ALTV  34681  trssfir1om  35122  trssfir1omregs  35132  br8  35800  br6  35801  br4  35802  fvtransport  36076  brcolinear2  36102  colineardim1  36105  fscgr  36124  idinside  36128  brsegle  36152  poimirlem28  37698  caures  37810  iscringd  38048  oposlem  39291  cdleme18d  40404  jm2.27  43111  ichexmpl2  47580  ichnreuop  47582  9gbo  47884  11gbo  47885