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  3545  vtocl3gaOLD  3547  axdc4uz  13925  wrdl3s3  14904  relexpindlem  15005  sqrtval  15179  sqreu  15303  coprmprod  16607  mreexexd  17589  iscatd2  17622  lmodprop2d  20862  neiptopnei  23052  hausnei  23248  isreg2  23297  regr1lem2  23660  ustval  24123  ustuqtop4  24165  axtgupdim2  28451  axtgeucl  28452  iscgra  28789  brbtwn  28879  ax5seg  28918  axlowdim  28941  axeuclidlem  28942  wlkonprop  29637  upgr2wlk  29647  upgrf1istrl  29682  elwspths2spth  29947  clwlkclwwlk  29981  clwwlknonel  30074  upgr4cycl4dv4e  30164  extwwlkfab  30331  nvi  30593  br8d  32588  xlt2addrd  32732  isslmd  33171  slmdlema  33172  constrllcllem  33735  constrcbvlem  33738  tgoldbachgt  34647  axtgupdim2ALTV  34652  br8  35736  br6  35737  br4  35738  fvtransport  36013  brcolinear2  36039  colineardim1  36042  fscgr  36061  idinside  36065  brsegle  36089  poimirlem28  37635  caures  37747  iscringd  37985  oposlem  39168  cdleme18d  40282  jm2.27  42990  ichexmpl2  47464  ichnreuop  47466  9gbo  47768  11gbo  47769