Theorem 3anbi13d 1439

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 1437	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  1443  ax12wdemo  2134  f1dom3el3dif  7290  xpord2lem  8168  xpord3lem  8175  frrlem1  8312  frrlem13  8324  wfrlem1OLD  8349  wfrlem3OLDa  8352  wfrlem15OLD  8364  cofsmo  10310  axdc3lem3  10493  axdc3lem4  10494  iscatd2  17725  psgnunilem1  19512  nn0gsumfz  20003  opprsubrg  20594  lsspropd  21017  mdetunilem3  22621  mdetunilem9  22627  smadiadetr  22682  lmres  23309  cnhaus  23363  regsep2  23385  dishaus  23391  ordthauslem  23392  nconnsubb  23432  pthaus  23647  txhaus  23656  xkohaus  23662  regr1lem  23748  ustval  24212  methaus  24534  metnrmlem3  24884  pmltpclem1  25484  brsslt  27831  axtgeucl  28481  iscgrad  28820  dfcgra2  28839  f1otrge  28881  axeuclidlem  28978  umgrvad2edg  29231  elwspths2spth  29988  upgr3v3e3cycl  30200  upgr4cycl4dv4e  30205  vdgn1frgrv2  30316  numclwlk1lem1  30389  ex-opab  30452  isnvlem  30630  ajval  30881  adjeu  31909  adjval  31910  adj1  31953  adjeq  31955  cnlnssadj  32100  br8d  32623  lt2addrd  32756  xlt2addrd  32763  crngmxidl  33498  constrconj  33787  measval  34200  loop1cycl  35143  br8  35757  br6  35758  br4  35759  brcgr3  36048  brsegle  36110  fvray  36143  linedegen  36145  fvline  36146  poimirlem28  37656  isopos  39182  hlsuprexch  39384  2llnjN  39570  2lplnj  39623  cdlemk42  40944  zindbi  42963  jm2.27  43025  nnoeomeqom  43330  tfsconcatrev  43366  rp-brsslt  43441  stoweidlem43  46063  fourierdlem42  46169  ichexmpl1  47461  vopnbgrel  47845  dfclnbgr6  47847  dfnbgr6  47848  cycl3grtri  47919  grimgrtri  47921  usgrgrtrirex  47922  grlimgrtri  47968  usgrexmpl1tri  47989  sepfsepc  48832  iscnrm3rlem8  48851  iscnrm3llem2  48854