Theorem 3anbi1d 1440

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

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

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 397  df-3an 1089

This theorem is referenced by:  vtocl3gaf  3568  vtocl3ga  3569  axdc4uz  13951  wrdl3s3  14915  relexpindlem  15012  sqrtval  15186  sqreu  15309  coprmprod  16600  mreexexd  17594  iscatd2  17627  lmodprop2d  20539  neiptopnei  22643  hausnei  22839  isreg2  22888  regr1lem2  23251  ustval  23714  ustuqtop4  23756  axtgupdim2  27760  axtgeucl  27761  iscgra  28098  brbtwn  28195  ax5seg  28234  axlowdim  28257  axeuclidlem  28258  wlkonprop  28953  upgr2wlk  28963  upgrf1istrl  28998  elwspths2spth  29259  clwlkclwwlk  29293  clwwlknonel  29386  upgr4cycl4dv4e  29476  extwwlkfab  29643  nvi  29905  br8d  31877  xlt2addrd  32009  isslmd  32388  slmdlema  32389  tgoldbachgt  33744  axtgupdim2ALTV  33749  br8  34795  br6  34796  br4  34797  fvtransport  35073  brcolinear2  35099  colineardim1  35102  fscgr  35121  idinside  35125  brsegle  35149  poimirlem28  36602  caures  36714  iscringd  36952  oposlem  38138  cdleme18d  39252  jm2.27  41829  ichexmpl2  46217  ichnreuop  46219  9gbo  46521  11gbo  46522