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  7206  xpord2lem  8075  xpord3lem  8082  frrlem1  8219  frrlem13  8231  cofsmo  10163  axdc3lem3  10346  axdc3lem4  10347  iscatd2  17587  psgnunilem1  19372  nn0gsumfz  19863  opprsubrg  20478  lsspropd  20921  mdetunilem3  22499  mdetunilem9  22505  smadiadetr  22560  lmres  23185  cnhaus  23239  regsep2  23261  dishaus  23267  ordthauslem  23268  nconnsubb  23308  pthaus  23523  txhaus  23532  xkohaus  23538  regr1lem  23624  ustval  24088  methaus  24406  metnrmlem3  24748  pmltpclem1  25347  brsslt  27696  axtgeucl  28417  iscgrad  28756  dfcgra2  28775  f1otrge  28817  axeuclidlem  28907  umgrvad2edg  29158  elwspths2spth  29912  upgr3v3e3cycl  30124  upgr4cycl4dv4e  30129  vdgn1frgrv2  30240  numclwlk1lem1  30313  ex-opab  30376  isnvlem  30554  ajval  30805  adjeu  31833  adjval  31834  adj1  31877  adjeq  31879  cnlnssadj  32024  br8d  32555  lt2addrd  32694  xlt2addrd  32702  crngmxidl  33406  constrconj  33712  constrllcllem  33719  constrcccllem  33721  constrcbvlem  33722  measval  34165  tz9.1regs  35067  loop1cycl  35110  br8  35729  br6  35730  br4  35731  brcgr3  36020  brsegle  36082  fvray  36115  linedegen  36117  fvline  36118  poimirlem28  37628  isopos  39159  hlsuprexch  39360  2llnjN  39546  2lplnj  39599  cdlemk42  40920  zindbi  42919  jm2.27  42981  nnoeomeqom  43285  tfsconcatrev  43321  rp-brsslt  43396  stoweidlem43  46024  fourierdlem42  46130  ichexmpl1  47453  vopnbgrel  47838  dfclnbgr6  47840  dfnbgr6  47841  cycl3grtri  47931  grimgrtri  47933  usgrgrtrirex  47934  grlimgrtri  47987  usgrexmpl1tri  48009  sepfsepc  48912  iscnrm3rlem8  48931  iscnrm3llem2  48934