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  7218  xpord2lem  8086  xpord3lem  8093  frrlem1  8230  frrlem13  8242  cofsmo  10185  axdc3lem3  10368  axdc3lem4  10369  iscatd2  17641  psgnunilem1  19462  nn0gsumfz  19953  opprsubrg  20564  lsspropd  21007  mdetunilem3  22592  mdetunilem9  22598  smadiadetr  22653  lmres  23278  cnhaus  23332  regsep2  23354  dishaus  23360  ordthauslem  23361  nconnsubb  23401  pthaus  23616  txhaus  23625  xkohaus  23631  regr1lem  23717  ustval  24181  methaus  24498  metnrmlem3  24840  pmltpclem1  25428  brslts  27771  bdayfinbndcbv  28475  bdayfinbndlem1  28476  bdayfinbndlem2  28477  axtgeucl  28557  iscgrad  28896  dfcgra2  28915  f1otrge  28957  axeuclidlem  29048  umgrvad2edg  29299  elwspths2spth  30056  upgr3v3e3cycl  30268  upgr4cycl4dv4e  30273  vdgn1frgrv2  30384  numclwlk1lem1  30457  ex-opab  30520  isnvlem  30699  ajval  30950  adjeu  31978  adjval  31979  adj1  32022  adjeq  32024  cnlnssadj  32169  br8d  32699  lt2addrd  32841  xlt2addrd  32850  crngmxidl  33547  constrconj  33908  constrllcllem  33915  constrcccllem  33917  constrcbvlem  33918  measval  34361  tz9.1regs  35297  loop1cycl  35338  br8  35957  br6  35958  br4  35959  brcgr3  36247  brsegle  36309  fvray  36342  linedegen  36344  fvline  36345  poimirlem28  37986  isopos  39643  hlsuprexch  39844  2llnjN  40030  2lplnj  40083  cdlemk42  41404  zindbi  43395  jm2.27  43457  nnoeomeqom  43761  tfsconcatrev  43797  rp-brsslt  43871  stoweidlem43  46492  fourierdlem42  46598  ichexmpl1  47944  vopnbgrel  48345  dfclnbgr6  48347  dfnbgr6  48348  cycl3grtri  48438  grimgrtri  48440  usgrgrtrirex  48441  grlimgrtri  48494  usgrexmpl1tri  48516  sepfsepc  49418  iscnrm3rlem8  49437  iscnrm3llem2  49440