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  3537  vtocl3gaOLD  3539  axdc4uz  13907  wrdl3s3  14885  relexpindlem  14986  sqrtval  15160  sqreu  15284  coprmprod  16588  mreexexd  17571  iscatd2  17604  lmodprop2d  20875  neiptopnei  23076  hausnei  23272  isreg2  23321  regr1lem2  23684  ustval  24147  ustuqtop4  24188  bdayfinbndcbv  28462  bdayfinbndlem1  28463  bdayfinbndlem2  28464  bdayfinbnd  28465  axtgupdim2  28543  axtgeucl  28544  iscgra  28881  brbtwn  28972  ax5seg  29011  axlowdim  29034  axeuclidlem  29035  wlkonprop  29730  upgr2wlk  29740  upgrf1istrl  29775  elwspths2spth  30043  clwlkclwwlk  30077  clwwlknonel  30170  upgr4cycl4dv4e  30260  extwwlkfab  30427  nvi  30689  br8d  32686  xlt2addrd  32839  isslmd  33284  slmdlema  33285  constrllcllem  33909  constrcbvlem  33912  tgoldbachgt  34820  axtgupdim2ALTV  34825  trssfir1om  35267  trssfir1omregs  35292  br8  35950  br6  35951  br4  35952  fvtransport  36226  brcolinear2  36252  colineardim1  36255  fscgr  36274  idinside  36278  brsegle  36302  poimirlem28  37849  caures  37961  iscringd  38199  oposlem  39442  cdleme18d  40555  jm2.27  43250  ichexmpl2  47716  ichnreuop  47718  9gbo  48020  11gbo  48021