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  2138  f1dom3el3dif  7203  xpord2lem  8072  xpord3lem  8079  frrlem1  8216  frrlem13  8228  cofsmo  10160  axdc3lem3  10343  axdc3lem4  10344  iscatd2  17587  psgnunilem1  19405  nn0gsumfz  19896  opprsubrg  20508  lsspropd  20951  mdetunilem3  22529  mdetunilem9  22535  smadiadetr  22590  lmres  23215  cnhaus  23269  regsep2  23291  dishaus  23297  ordthauslem  23298  nconnsubb  23338  pthaus  23553  txhaus  23562  xkohaus  23568  regr1lem  23654  ustval  24118  methaus  24435  metnrmlem3  24777  pmltpclem1  25376  brsslt  27725  axtgeucl  28450  iscgrad  28789  dfcgra2  28808  f1otrge  28850  axeuclidlem  28940  umgrvad2edg  29191  elwspths2spth  29948  upgr3v3e3cycl  30160  upgr4cycl4dv4e  30165  vdgn1frgrv2  30276  numclwlk1lem1  30349  ex-opab  30412  isnvlem  30590  ajval  30841  adjeu  31869  adjval  31870  adj1  31913  adjeq  31915  cnlnssadj  32060  br8d  32591  lt2addrd  32734  xlt2addrd  32742  crngmxidl  33434  constrconj  33758  constrllcllem  33765  constrcccllem  33767  constrcbvlem  33768  measval  34211  tz9.1regs  35130  loop1cycl  35181  br8  35800  br6  35801  br4  35802  brcgr3  36088  brsegle  36150  fvray  36183  linedegen  36185  fvline  36186  poimirlem28  37696  isopos  39227  hlsuprexch  39428  2llnjN  39614  2lplnj  39667  cdlemk42  40988  zindbi  42987  jm2.27  43049  nnoeomeqom  43353  tfsconcatrev  43389  rp-brsslt  43464  stoweidlem43  46089  fourierdlem42  46195  ichexmpl1  47508  vopnbgrel  47893  dfclnbgr6  47895  dfnbgr6  47896  cycl3grtri  47986  grimgrtri  47988  usgrgrtrirex  47989  grlimgrtri  48042  usgrexmpl1tri  48064  sepfsepc  48967  iscnrm3rlem8  48986  iscnrm3llem2  48989