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  2133  f1dom3el3dif  7123  frrlem1  8073  frrlem13  8085  wfrlem1OLD  8110  wfrlem3OLDa  8113  wfrlem15OLD  8125  cofsmo  9956  axdc3lem3  10139  axdc3lem4  10140  iscatd2  17307  psgnunilem1  19016  nn0gsumfz  19500  opprsubrg  19960  lsspropd  20194  mdetunilem3  21671  mdetunilem9  21677  smadiadetr  21732  lmres  22359  cnhaus  22413  regsep2  22435  dishaus  22441  ordthauslem  22442  nconnsubb  22482  pthaus  22697  txhaus  22706  xkohaus  22712  regr1lem  22798  ustval  23262  methaus  23582  metnrmlem3  23930  pmltpclem1  24517  axtgeucl  26737  iscgrad  27076  dfcgra2  27095  f1otrge  27137  axeuclidlem  27233  umgrvad2edg  27483  elwspths2spth  28233  upgr3v3e3cycl  28445  upgr4cycl4dv4e  28450  vdgn1frgrv2  28561  numclwlk1lem1  28634  ex-opab  28697  isnvlem  28873  ajval  29124  adjeu  30152  adjval  30153  adj1  30196  adjeq  30198  cnlnssadj  30343  br8d  30851  lt2addrd  30976  xlt2addrd  30983  measval  32066  loop1cycl  32999  br8  33629  br6  33630  br4  33631  xpord2lem  33716  xpord3lem  33722  brsslt  33907  brcgr3  34275  brsegle  34337  fvray  34370  linedegen  34372  fvline  34373  poimirlem28  35732  isopos  37121  hlsuprexch  37322  2llnjN  37508  2lplnj  37561  cdlemk42  38882  zindbi  40684  jm2.27  40746  stoweidlem43  43474  fourierdlem42  43580  ichexmpl1  44809  sepfsepc  46109  iscnrm3rlem8  46129  iscnrm3llem2  46132