Theorem 3anbi1d 1436

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  vtocl3gaf  3576  axdc4uz  13351  wrdl3s3  14325  relexpindlem  14421  sqrtval  14595  sqreu  14719  coprmprod  16004  mreexexd  16918  iscatd2  16951  lmodprop2d  19695  neiptopnei  21739  hausnei  21935  isreg2  21984  regr1lem2  22347  ustval  22810  ustuqtop4  22852  axtgupdim2  26256  axtgeucl  26257  iscgra  26594  brbtwn  26684  ax5seg  26723  axlowdim  26746  axeuclidlem  26747  wlkonprop  27439  upgr2wlk  27449  upgrf1istrl  27484  elwspths2spth  27745  clwlkclwwlk  27779  clwwlknonel  27873  upgr4cycl4dv4e  27963  extwwlkfab  28130  nvi  28390  br8d  30360  xlt2addrd  30481  isslmd  30830  slmdlema  30831  tgoldbachgt  31934  axtgupdim2ALTV  31939  br8  32992  br6  32993  br4  32994  fvtransport  33493  brcolinear2  33519  colineardim1  33522  fscgr  33541  idinside  33545  brsegle  33569  poimirlem28  34919  caures  35034  iscringd  35275  oposlem  36317  cdleme18d  37430  jm2.27  39603  ichexmpl2  43631  ichnreuop  43633  9gbo  43938  11gbo  43939