Theorem 3anbi2d 1404

Description: Deduction adding conjuncts to an equivalence. (Contributed by NM, 8-Sep-2006.)

Hypothesis

Ref	Expression
3anbi1d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
3anbi2d	⊢ (𝜑 → ((𝜃 ∧ 𝜓 ∧ 𝜏) ↔ (𝜃 ∧ 𝜒 ∧ 𝜏)))

Proof of Theorem 3anbi2d

Step	Hyp	Ref	Expression
1		biidd 252	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜃))
2		3anbi1d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	3anbi12d 1400	1 ⊢ (𝜑 → ((𝜃 ∧ 𝜓 ∧ 𝜏) ↔ (𝜃 ∧ 𝜒 ∧ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 196   ∧ w3a 1037

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 197  df-an 386  df-3an 1039

This theorem is referenced by:  vtocl3gaf  3275  offval22  7253  ereq2  7750  wrdl3s3  13705  mhmlem  17535  isdrngrd  18773  lmodlema  18868  mdetunilem9  20426  neiptoptop  20935  neiptopnei  20936  hausnei  21132  regr1lem2  21543  ustuqtop4  22048  utopsnneiplem  22051  axtg5seg  25364  axtgupdim2  25370  axtgeucl  25371  brbtwn  25779  axlowdim  25841  axeuclidlem  25842  incistruhgr  25974  issubgr2  26164  wwlksnwwlksnon  26810  upgr4cycl4dv4e  27045  isnvlem  27465  csmdsymi  29193  br8d  29422  slmdlema  29756  carsgmon  30376  sitgclg  30404  tgoldbachgt  30741  axtgupdim2OLD  30746  bnj852  30991  bnj18eq1  30997  bnj938  31007  bnj983  31021  bnj1318  31093  bnj1326  31094  cvmlift3lem4  31304  cvmlift3  31310  br8  31646  br6  31647  br4  31648  brcolinear2  32165  colineardim1  32168  brfs  32186  fscgr  32187  btwnconn1lem7  32200  brsegle  32215  unblimceq0  32498  sdclem2  33538  sdclem1  33539  sdc  33540  fdc  33541  cdleme18d  35582  cdlemk35s  36225  cdlemk39s  36227  monotoddzz  37508  jm2.27  37575  mendlmod  37763  fiiuncl  39234  wessf1ornlem  39371  fmulcl  39813  fmuldfeqlem1  39814  fprodcncf  40114  dvmptfprodlem  40159  dvmptfprod  40160  dvnprodlem2  40162  stoweidlem6  40223  stoweidlem8  40225  stoweidlem31  40248  stoweidlem34  40251  stoweidlem43  40260  stoweidlem52  40269  fourierdlem41  40365  fourierdlem48  40371  fourierdlem49  40372  ovnsubaddlem1  40784  9gbo  41662  11gbo  41663  lmod1  42281