Theorem 3anbi1d 1438

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

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

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 396  df-3an 1087

This theorem is referenced by:  vtocl3gaf  3506  vtocl3ga  3507  axdc4uz  13632  wrdl3s3  14605  relexpindlem  14702  sqrtval  14876  sqreu  15000  coprmprod  16294  mreexexd  17274  iscatd2  17307  lmodprop2d  20100  neiptopnei  22191  hausnei  22387  isreg2  22436  regr1lem2  22799  ustval  23262  ustuqtop4  23304  axtgupdim2  26736  axtgeucl  26737  iscgra  27074  brbtwn  27170  ax5seg  27209  axlowdim  27232  axeuclidlem  27233  wlkonprop  27928  upgr2wlk  27938  upgrf1istrl  27973  elwspths2spth  28233  clwlkclwwlk  28267  clwwlknonel  28360  upgr4cycl4dv4e  28450  extwwlkfab  28617  nvi  28877  br8d  30851  xlt2addrd  30983  isslmd  31357  slmdlema  31358  tgoldbachgt  32543  axtgupdim2ALTV  32548  br8  33629  br6  33630  br4  33631  fvtransport  34261  brcolinear2  34287  colineardim1  34290  fscgr  34309  idinside  34313  brsegle  34337  poimirlem28  35732  caures  35845  iscringd  36083  oposlem  37123  cdleme18d  38236  jm2.27  40746  ichexmpl2  44810  ichnreuop  44812  9gbo  45114  11gbo  45115