Theorem 3anbi13d 1436

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  3anbi3d  1440  ax12wdemo  2126  f1dom3el3dif  7162  frrlem1  8122  frrlem13  8134  wfrlem1OLD  8159  wfrlem3OLDa  8162  wfrlem15OLD  8174  cofsmo  10053  axdc3lem3  10236  axdc3lem4  10237  iscatd2  17418  psgnunilem1  19129  nn0gsumfz  19613  opprsubrg  20073  lsspropd  20307  mdetunilem3  21791  mdetunilem9  21797  smadiadetr  21852  lmres  22479  cnhaus  22533  regsep2  22555  dishaus  22561  ordthauslem  22562  nconnsubb  22602  pthaus  22817  txhaus  22826  xkohaus  22832  regr1lem  22918  ustval  23382  methaus  23704  metnrmlem3  24052  pmltpclem1  24640  axtgeucl  26861  iscgrad  27200  dfcgra2  27219  f1otrge  27261  axeuclidlem  27358  umgrvad2edg  27608  elwspths2spth  28360  upgr3v3e3cycl  28572  upgr4cycl4dv4e  28577  vdgn1frgrv2  28688  numclwlk1lem1  28761  ex-opab  28824  isnvlem  29000  ajval  29251  adjeu  30279  adjval  30280  adj1  30323  adjeq  30325  cnlnssadj  30470  br8d  30978  lt2addrd  31102  xlt2addrd  31109  measval  32194  loop1cycl  33127  br8  33751  br6  33752  br4  33753  xpord2lem  33817  xpord3lem  33823  brsslt  34008  brcgr3  34376  brsegle  34438  fvray  34471  linedegen  34473  fvline  34474  poimirlem28  35833  isopos  37220  hlsuprexch  37421  2llnjN  37607  2lplnj  37660  cdlemk42  38981  zindbi  40792  jm2.27  40854  stoweidlem43  43619  fourierdlem42  43725  ichexmpl1  44961  sepfsepc  46261  iscnrm3rlem8  46281  iscnrm3llem2  46284