Theorem 3anbi13d 1438

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 1436	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  1442  ax12wdemo  2135  f1dom3el3dif  7306  xpord2lem  8183  xpord3lem  8190  frrlem1  8327  frrlem13  8339  wfrlem1OLD  8364  wfrlem3OLDa  8367  wfrlem15OLD  8379  cofsmo  10338  axdc3lem3  10521  axdc3lem4  10522  iscatd2  17739  psgnunilem1  19535  nn0gsumfz  20026  opprsubrg  20621  lsspropd  21039  mdetunilem3  22641  mdetunilem9  22647  smadiadetr  22702  lmres  23329  cnhaus  23383  regsep2  23405  dishaus  23411  ordthauslem  23412  nconnsubb  23452  pthaus  23667  txhaus  23676  xkohaus  23682  regr1lem  23768  ustval  24232  methaus  24554  metnrmlem3  24902  pmltpclem1  25502  brsslt  27848  axtgeucl  28498  iscgrad  28837  dfcgra2  28856  f1otrge  28898  axeuclidlem  28995  umgrvad2edg  29248  elwspths2spth  30000  upgr3v3e3cycl  30212  upgr4cycl4dv4e  30217  vdgn1frgrv2  30328  numclwlk1lem1  30401  ex-opab  30464  isnvlem  30642  ajval  30893  adjeu  31921  adjval  31922  adj1  31965  adjeq  31967  cnlnssadj  32112  br8d  32632  lt2addrd  32758  xlt2addrd  32765  crngmxidl  33462  constrconj  33735  measval  34162  loop1cycl  35105  br8  35718  br6  35719  br4  35720  brcgr3  36010  brsegle  36072  fvray  36105  linedegen  36107  fvline  36108  poimirlem28  37608  isopos  39136  hlsuprexch  39338  2llnjN  39524  2lplnj  39577  cdlemk42  40898  zindbi  42903  jm2.27  42965  nnoeomeqom  43274  tfsconcatrev  43310  rp-brsslt  43385  stoweidlem43  45964  fourierdlem42  46070  ichexmpl1  47343  vopnbgrel  47726  dfclnbgr6  47728  dfnbgr6  47729  grimgrtri  47798  usgrgrtrirex  47799  grlimgrtri  47820  usgrexmpl1tri  47840  sepfsepc  48607  iscnrm3rlem8  48627  iscnrm3llem2  48630