Theorem 3anbi13d 1441

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  3anbi3d  1445  ax12wdemo  2141  f1dom3el3dif  7225  xpord2lem  8094  xpord3lem  8101  frrlem1  8238  frrlem13  8250  cofsmo  10191  axdc3lem3  10374  axdc3lem4  10375  iscatd2  17616  psgnunilem1  19434  nn0gsumfz  19925  opprsubrg  20538  lsspropd  20981  mdetunilem3  22570  mdetunilem9  22576  smadiadetr  22631  lmres  23256  cnhaus  23310  regsep2  23332  dishaus  23338  ordthauslem  23339  nconnsubb  23379  pthaus  23594  txhaus  23603  xkohaus  23609  regr1lem  23695  ustval  24159  methaus  24476  metnrmlem3  24818  pmltpclem1  25417  brslts  27770  bdayfinbndcbv  28474  bdayfinbndlem1  28475  bdayfinbndlem2  28476  axtgeucl  28556  iscgrad  28895  dfcgra2  28914  f1otrge  28956  axeuclidlem  29047  umgrvad2edg  29298  elwspths2spth  30055  upgr3v3e3cycl  30267  upgr4cycl4dv4e  30272  vdgn1frgrv2  30383  numclwlk1lem1  30456  ex-opab  30519  isnvlem  30698  ajval  30949  adjeu  31977  adjval  31978  adj1  32021  adjeq  32023  cnlnssadj  32168  br8d  32698  lt2addrd  32841  xlt2addrd  32850  crngmxidl  33562  constrconj  33923  constrllcllem  33930  constrcccllem  33932  constrcbvlem  33933  measval  34376  tz9.1regs  35312  loop1cycl  35353  br8  35972  br6  35973  br4  35974  brcgr3  36262  brsegle  36324  fvray  36357  linedegen  36359  fvline  36360  poimirlem28  37899  isopos  39556  hlsuprexch  39757  2llnjN  39943  2lplnj  39996  cdlemk42  41317  zindbi  43303  jm2.27  43365  nnoeomeqom  43669  tfsconcatrev  43705  rp-brsslt  43779  stoweidlem43  46401  fourierdlem42  46507  ichexmpl1  47829  vopnbgrel  48214  dfclnbgr6  48216  dfnbgr6  48217  cycl3grtri  48307  grimgrtri  48309  usgrgrtrirex  48310  grlimgrtri  48363  usgrexmpl1tri  48385  sepfsepc  49287  iscnrm3rlem8  49306  iscnrm3llem2  49309