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  2136  f1dom3el3dif  7247  xpord2lem  8124  xpord3lem  8131  frrlem1  8268  frrlem13  8280  cofsmo  10229  axdc3lem3  10412  axdc3lem4  10413  iscatd2  17649  psgnunilem1  19430  nn0gsumfz  19921  opprsubrg  20509  lsspropd  20931  mdetunilem3  22508  mdetunilem9  22514  smadiadetr  22569  lmres  23194  cnhaus  23248  regsep2  23270  dishaus  23276  ordthauslem  23277  nconnsubb  23317  pthaus  23532  txhaus  23541  xkohaus  23547  regr1lem  23633  ustval  24097  methaus  24415  metnrmlem3  24757  pmltpclem1  25356  brsslt  27704  axtgeucl  28406  iscgrad  28745  dfcgra2  28764  f1otrge  28806  axeuclidlem  28896  umgrvad2edg  29147  elwspths2spth  29904  upgr3v3e3cycl  30116  upgr4cycl4dv4e  30121  vdgn1frgrv2  30232  numclwlk1lem1  30305  ex-opab  30368  isnvlem  30546  ajval  30797  adjeu  31825  adjval  31826  adj1  31869  adjeq  31871  cnlnssadj  32016  br8d  32545  lt2addrd  32681  xlt2addrd  32689  crngmxidl  33447  constrconj  33742  constrllcllem  33749  constrcccllem  33751  constrcbvlem  33752  measval  34195  loop1cycl  35131  br8  35750  br6  35751  br4  35752  brcgr3  36041  brsegle  36103  fvray  36136  linedegen  36138  fvline  36139  poimirlem28  37649  isopos  39180  hlsuprexch  39382  2llnjN  39568  2lplnj  39621  cdlemk42  40942  zindbi  42942  jm2.27  43004  nnoeomeqom  43308  tfsconcatrev  43344  rp-brsslt  43419  stoweidlem43  46048  fourierdlem42  46154  ichexmpl1  47474  vopnbgrel  47858  dfclnbgr6  47860  dfnbgr6  47861  cycl3grtri  47950  grimgrtri  47952  usgrgrtrirex  47953  grlimgrtri  47999  usgrexmpl1tri  48020  sepfsepc  48920  iscnrm3rlem8  48939  iscnrm3llem2  48942