Theorem 3anbi13d 1459

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1098

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 209  df-an 400  df-3an 1100

This theorem is referenced by:  3anbi3d  1463  ax12wdemo  2169  f1dom3el3dif  7253  xpord2lem  8122  xpord3lem  8129  frrlem1  8267  frrlem13  8279  cofsmo  10226  axdc3lem3  10409  axdc3lem4  10410  iscatd2  17713  psgnunilem1  19533  nn0gsumfz  20024  opprsubrg  20639  lsspropd  21081  mdetunilem3  22671  mdetunilem9  22677  smadiadetr  22732  lmres  23357  cnhaus  23411  regsep2  23433  dishaus  23439  ordthauslem  23440  nconnsubb  23480  pthaus  23695  txhaus  23704  xkohaus  23710  regr1lem  23796  ustval  24260  methaus  24577  metnrmlem3  24919  pmltpclem1  25507  brslts  27852  bdayfinbndcbv  28556  bdayfinbndlem1  28557  bdayfinbndlem2  28558  axtgeucl  28638  iscgrad  29002  dfcgra2  29021  f1otrge  29069  axeuclidlem  29160  umgrvad2edg  29411  elwspths2spth  30167  upgr3v3e3cycl  30379  upgr4cycl4dv4e  30384  vdgn1frgrv2  30495  numclwlk1lem1  30568  ex-opab  30631  isnvlem  30810  ajval  31061  adjeu  32089  adjval  32090  adj1  32133  adjeq  32135  cnlnssadj  32280  br8d  32807  lt2addrd  32949  xlt2addrd  32958  crngmxidl  33654  constrconj  34039  constrllcllem  34046  constrcccllem  34048  constrcbvlem  34049  measval  34492  tz9.1regs  35427  loop1cycl  35484  br8  36103  br6  36104  br4  36105  brcgr3  36393  brsegle  36455  fvray  36488  linedegen  36490  fvline  36491  poimirlem28  38144  isopos  39801  hlsuprexch  40002  2llnjN  40188  2lplnj  40241  cdlemk42  41562  zindbi  43520  jm2.27  43582  nnoeomeqom  43886  tfsconcatrev  43922  rp-brsslt  43996  stoweidlem43  46614  fourierdlem42  46720  ichexmpl1  48072  vopnbgrel  48473  dfclnbgr6  48475  dfnbgr6  48476  cycl3grtri  48566  grimgrtri  48568  usgrgrtrirex  48569  grlimgrtri  48622  usgrexmpl1tri  48644  sepfsepc  49546  iscnrm3rlem8  49565  iscnrm3llem2  49568