Theorem 3anbi13d 1440

Description: Deduction conjoining and adding a conjunct to equivalences. (Contributed by NM, 8-Sep-2006.)

Hypotheses

Ref	Expression
3anbi12d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3anbi12d.2	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Assertion

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

Proof of Theorem 3anbi13d

Step	Hyp	Ref	Expression
1		3anbi12d.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		biidd 262	. 2 ⊢ (𝜑 → (𝜂 ↔ 𝜂))
3		3anbi12d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	1, 2, 3	3anbi123d 1438	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:  3anbi3d  1444  ax12wdemo  2136  f1dom3el3dif  7267  xpord2lem  8146  xpord3lem  8153  frrlem1  8290  frrlem13  8302  wfrlem1OLD  8327  wfrlem3OLDa  8330  wfrlem15OLD  8342  cofsmo  10288  axdc3lem3  10471  axdc3lem4  10472  iscatd2  17698  psgnunilem1  19479  nn0gsumfz  19970  opprsubrg  20558  lsspropd  20980  mdetunilem3  22557  mdetunilem9  22563  smadiadetr  22618  lmres  23243  cnhaus  23297  regsep2  23319  dishaus  23325  ordthauslem  23326  nconnsubb  23366  pthaus  23581  txhaus  23590  xkohaus  23596  regr1lem  23682  ustval  24146  methaus  24464  metnrmlem3  24806  pmltpclem1  25406  brsslt  27754  axtgeucl  28456  iscgrad  28795  dfcgra2  28814  f1otrge  28856  axeuclidlem  28946  umgrvad2edg  29197  elwspths2spth  29954  upgr3v3e3cycl  30166  upgr4cycl4dv4e  30171  vdgn1frgrv2  30282  numclwlk1lem1  30355  ex-opab  30418  isnvlem  30596  ajval  30847  adjeu  31875  adjval  31876  adj1  31919  adjeq  31921  cnlnssadj  32066  br8d  32595  lt2addrd  32733  xlt2addrd  32741  crngmxidl  33489  constrconj  33784  constrllcllem  33791  constrcccllem  33793  constrcbvlem  33794  measval  34234  loop1cycl  35164  br8  35778  br6  35779  br4  35780  brcgr3  36069  brsegle  36131  fvray  36164  linedegen  36166  fvline  36167  poimirlem28  37677  isopos  39203  hlsuprexch  39405  2llnjN  39591  2lplnj  39644  cdlemk42  40965  zindbi  42937  jm2.27  42999  nnoeomeqom  43303  tfsconcatrev  43339  rp-brsslt  43414  stoweidlem43  46039  fourierdlem42  46145  ichexmpl1  47450  vopnbgrel  47834  dfclnbgr6  47836  dfnbgr6  47837  cycl3grtri  47926  grimgrtri  47928  usgrgrtrirex  47929  grlimgrtri  47975  usgrexmpl1tri  47996  sepfsepc  48869  iscnrm3rlem8  48888  iscnrm3llem2  48891