Theorem 3anbi13d 1466

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 265	. 2 ⊢ (𝜑 → (𝜂 ↔ 𝜂))
3		3anbi12d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
4	1, 2, 3	3anbi123d 1464	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜂 ∧ 𝜃) ↔ (𝜒 ∧ 𝜂 ∧ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  3anbi3d  1470  ax12wdemo  2170  f1dom3el3dif  7267  xpord2lem  8134  xpord3lem  8141  frrlem1  8279  frrlem13  8291  cofsmo  10248  axdc3lem3  10431  axdc3lem4  10432  iscatd2  17732  psgnunilem1  19558  nn0gsumfz  20049  opprsubrg  20692  lsspropd  21138  mdetunilem3  22771  mdetunilem9  22777  smadiadetr  22832  lmres  23457  cnhaus  23511  regsep2  23533  dishaus  23539  ordthauslem  23540  nconnsubb  23580  pthaus  23795  txhaus  23804  xkohaus  23810  regr1lem  23896  ustval  24360  methaus  24677  metnrmlem3  25019  pmltpclem1  25607  brslts  27955  bdayfinbndcbv  28659  bdayfinbndlem1  28660  bdayfinbndlem2  28661  axtgeucl  28741  iscgrad  29122  dfcgra2  29141  f1otrge  29221  axeuclidlem  29312  umgrvad2edg  29563  elwspths2spth  30319  upgr3v3e3cycl  30531  upgr4cycl4dv4e  30536  vdgn1frgrv2  30647  numclwlk1lem1  30720  ex-opab  30783  isnvlem  30962  ajval  31213  adjeu  32241  adjval  32242  adj1  32285  adjeq  32287  cnlnssadj  32432  br8d  32953  lt2addrd  33095  xlt2addrd  33104  crngmxidl  33752  constrconj  34135  constrllcllem  34142  constrcccllem  34144  constrcbvlem  34145  measval  34588  tz9.1regs  35547  loop1cycl  35629  br8  36248  br6  36249  br4  36250  brcgr3  36538  brsegle  36600  fvray  36633  linedegen  36635  fvline  36636  poimirlem28  38299  isopos  39954  hlsuprexch  40155  2llnjN  40341  2lplnj  40394  cdlemk42  41715  zindbi  43673  jm2.27  43735  nnoeomeqom  44039  tfsconcatrev  44075  rp-brsslt  44149  stoweidlem43  46757  fourierdlem42  46863  ichexmpl1  48218  vopnbgrel  48619  dfclnbgr6  48621  dfnbgr6  48622  cycl3grtri  48712  grimgrtri  48714  usgrgrtrirex  48715  grlimgrtri  48768  usgrexmpl1tri  48790  sepfsepc  49706  iscnrm3rlem8  49725  iscnrm3llem2  49728