Theorem 3anbi13d 1441

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 1439	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜂 ∧ 𝜃) ↔ (𝜒 ∧ 𝜂 ∧ 𝜏)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ w3a 1087

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 1089

This theorem is referenced by:  3anbi3d  1445  ax12wdemo  2141  f1dom3el3dif  7224  xpord2lem  8092  xpord3lem  8099  frrlem1  8236  frrlem13  8248  cofsmo  10191  axdc3lem3  10374  axdc3lem4  10375  iscatd2  17647  psgnunilem1  19468  nn0gsumfz  19959  opprsubrg  20570  lsspropd  21012  mdetunilem3  22579  mdetunilem9  22585  smadiadetr  22640  lmres  23265  cnhaus  23319  regsep2  23341  dishaus  23347  ordthauslem  23348  nconnsubb  23388  pthaus  23603  txhaus  23612  xkohaus  23618  regr1lem  23704  ustval  24168  methaus  24485  metnrmlem3  24827  pmltpclem1  25415  brslts  27754  bdayfinbndcbv  28458  bdayfinbndlem1  28459  bdayfinbndlem2  28460  axtgeucl  28540  iscgrad  28879  dfcgra2  28898  f1otrge  28940  axeuclidlem  29031  umgrvad2edg  29282  elwspths2spth  30038  upgr3v3e3cycl  30250  upgr4cycl4dv4e  30255  vdgn1frgrv2  30366  numclwlk1lem1  30439  ex-opab  30502  isnvlem  30681  ajval  30932  adjeu  31960  adjval  31961  adj1  32004  adjeq  32006  cnlnssadj  32151  br8d  32681  lt2addrd  32823  xlt2addrd  32832  crngmxidl  33529  constrconj  33889  constrllcllem  33896  constrcccllem  33898  constrcbvlem  33899  measval  34342  tz9.1regs  35278  loop1cycl  35319  br8  35938  br6  35939  br4  35940  brcgr3  36228  brsegle  36290  fvray  36323  linedegen  36325  fvline  36326  poimirlem28  37969  isopos  39626  hlsuprexch  39827  2llnjN  40013  2lplnj  40066  cdlemk42  41387  zindbi  43374  jm2.27  43436  nnoeomeqom  43740  tfsconcatrev  43776  rp-brsslt  43850  stoweidlem43  46471  fourierdlem42  46577  ichexmpl1  47929  vopnbgrel  48330  dfclnbgr6  48332  dfnbgr6  48333  cycl3grtri  48423  grimgrtri  48425  usgrgrtrirex  48426  grlimgrtri  48479  usgrexmpl1tri  48501  sepfsepc  49403  iscnrm3rlem8  49422  iscnrm3llem2  49425