Theorem 3anbi13d 1433

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ w3a 1082

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 209  df-an 399  df-3an 1084

This theorem is referenced by:  3anbi3d  1437  ax12wdemo  2138  f1dom3el3dif  7020  wfrlem1  7947  wfrlem3a  7950  wfrlem15  7962  cofsmo  9684  axdc3lem3  9867  axdc3lem4  9868  iscatd2  16947  psgnunilem1  18616  nn0gsumfz  19099  opprsubrg  19551  lsspropd  19784  mdetunilem3  21218  mdetunilem9  21224  smadiadetr  21279  lmres  21903  cnhaus  21957  regsep2  21979  dishaus  21985  ordthauslem  21986  nconnsubb  22026  pthaus  22241  txhaus  22250  xkohaus  22256  regr1lem  22342  ustval  22806  methaus  23125  metnrmlem3  23464  pmltpclem1  24044  axtgeucl  26256  iscgrad  26595  dfcgra2  26614  f1otrge  26656  axeuclidlem  26746  umgrvad2edg  26993  elwspths2spth  27744  upgr3v3e3cycl  27957  upgr4cycl4dv4e  27962  vdgn1frgrv2  28073  numclwlk1lem1  28146  ex-opab  28209  isnvlem  28385  ajval  28636  adjeu  29664  adjval  29665  adj1  29708  adjeq  29710  cnlnssadj  29855  br8d  30361  lt2addrd  30475  xlt2addrd  30482  measval  31478  loop1cycl  32405  br8  33013  br6  33014  br4  33015  frrlem1  33144  frrlem13  33156  brsslt  33275  brcgr3  33528  brsegle  33590  fvray  33623  linedegen  33625  fvline  33626  poimirlem28  34955  isopos  36349  hlsuprexch  36550  2llnjN  36736  2lplnj  36789  cdlemk42  38110  zindbi  39619  jm2.27  39681  stoweidlem43  42402  fourierdlem42  42508  ichexmpl1  43705