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  2140  f1dom3el3dif  7213  xpord2lem  8082  xpord3lem  8089  frrlem1  8226  frrlem13  8238  cofsmo  10177  axdc3lem3  10360  axdc3lem4  10361  iscatd2  17602  psgnunilem1  19420  nn0gsumfz  19911  opprsubrg  20524  lsspropd  20967  mdetunilem3  22556  mdetunilem9  22562  smadiadetr  22617  lmres  23242  cnhaus  23296  regsep2  23318  dishaus  23324  ordthauslem  23325  nconnsubb  23365  pthaus  23580  txhaus  23589  xkohaus  23595  regr1lem  23681  ustval  24145  methaus  24462  metnrmlem3  24804  pmltpclem1  25403  brsslt  27752  axtgeucl  28493  iscgrad  28832  dfcgra2  28851  f1otrge  28893  axeuclidlem  28984  umgrvad2edg  29235  elwspths2spth  29992  upgr3v3e3cycl  30204  upgr4cycl4dv4e  30209  vdgn1frgrv2  30320  numclwlk1lem1  30393  ex-opab  30456  isnvlem  30634  ajval  30885  adjeu  31913  adjval  31914  adj1  31957  adjeq  31959  cnlnssadj  32104  br8d  32635  lt2addrd  32779  xlt2addrd  32788  crngmxidl  33499  constrconj  33851  constrllcllem  33858  constrcccllem  33860  constrcbvlem  33861  measval  34304  tz9.1regs  35239  loop1cycl  35280  br8  35899  br6  35900  br4  35901  brcgr3  36189  brsegle  36251  fvray  36284  linedegen  36286  fvline  36287  poimirlem28  37788  isopos  39379  hlsuprexch  39580  2llnjN  39766  2lplnj  39819  cdlemk42  41140  zindbi  43130  jm2.27  43192  nnoeomeqom  43496  tfsconcatrev  43532  rp-brsslt  43606  stoweidlem43  46229  fourierdlem42  46335  ichexmpl1  47657  vopnbgrel  48042  dfclnbgr6  48044  dfnbgr6  48045  cycl3grtri  48135  grimgrtri  48137  usgrgrtrirex  48138  grlimgrtri  48191  usgrexmpl1tri  48213  sepfsepc  49115  iscnrm3rlem8  49134  iscnrm3llem2  49137