Theorem 3anbi123d 1435

Description: Deduction joining 3 equivalences to form equivalence of conjunctions. (Contributed by NM, 22-Apr-1994.)

Hypotheses

Ref	Expression
bi3d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
bi3d.2	⊢ (𝜑 → (𝜃 ↔ 𝜏))
bi3d.3	⊢ (𝜑 → (𝜂 ↔ 𝜁))

Assertion

Ref	Expression
3anbi123d	⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜁)))

Proof of Theorem 3anbi123d

Step	Hyp	Ref	Expression
1		bi3d.1	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		bi3d.2	. . . 4 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
3	1, 2	anbi12d 631	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏)))
4		bi3d.3	. . 3 ⊢ (𝜑 → (𝜂 ↔ 𝜁))
5	3, 4	anbi12d 631	. 2 ⊢ (𝜑 → (((𝜓 ∧ 𝜃) ∧ 𝜂) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁)))
6		df-3an 1088	. 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂))
7		df-3an 1088	. 2 ⊢ ((𝜒 ∧ 𝜏 ∧ 𝜁) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁))
8	5, 6, 7	3bitr4g 314	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜁)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  3anbi12d  1436  3anbi13d  1437  3anbi23d  1438  ax12wdemo  2132  limeq  6282  f13dfv  7155  epne3  7632  oteqimp  7859  csbfrecsg  8109  frrlem1  8111  frrlem13  8123  wfrlem1OLD  8148  wfrlem15OLD  8163  smoeq  8190  ereq1  8514  sbthfi  8994  indexfi  9136  hartogslem1  9310  brttrcl2  9481  ssttrcl  9482  ttrcltr  9483  ttrclss  9487  ttrclselem2  9493  tz9.1  9496  updjud  9701  alephval3  9875  cofsmo  10034  cfsmolem  10035  alephsing  10041  axdc3lem2  10216  axdc3lem3  10217  axdc3  10219  axdc4lem  10220  zornn0g  10270  fpwwe2lem4  10399  canthwelem  10415  canthwe  10416  pwfseqlem4a  10426  pwfseqlem4  10427  elwina  10451  elina  10452  iswun  10469  elgrug  10557  iccshftr  13227  iccshftl  13229  iccdil  13231  icccntr  13233  fzaddel  13299  elfzomelpfzo  13500  axdc4uzlem  13712  wrdl1s1  14328  wwlktovf  14680  wwlktovf1  14681  wwlktovfo  14682  wrd2f1tovbij  14684  dfrtrcl2  14782  sqrmo  14972  resqrtcl  14974  resqrtthlem  14975  sqrtneg  14988  sqreu  15081  sqrtthlem  15083  eqsqrtd  15088  prodeq1f  15627  zprod  15656  divalglem10  16120  dfgcd2  16263  coprmprod  16375  pythagtriplem18  16542  pythagtriplem19  16543  prmgaplem3  16763  prmgaplem4  16764  isstruct2  16859  imasval  17231  mreexexlemd  17362  catidd  17398  iscatd2  17399  subsubc  17577  isfunc  17588  funcres2b  17621  ispos  18041  posi  18044  isposd  18050  pospropd  18054  isps  18295  imasmnd2  18431  sgrp2rid2ex  18575  imasgrp2  18699  psgnunilem3  19113  isringd  19833  imasring  19867  isdrngd  20025  islmod  20136  lmodlema  20137  islmodd  20138  lmodprop2d  20194  lmhmpropd  20344  isphl  20842  isphld  20868  phlpropd  20869  assapropd  21085  mdetunilem3  21772  mdetunilem9  21778  fiinopn  22059  iscldtop  22255  lmfval  22392  connsuba  22580  1stcfb  22605  2ndcctbss  22615  subislly  22641  ptval  22730  elpt  22732  elptr  22733  upxp  22783  isfbas  22989  ustval  23363  isust  23364  ustincl  23368  ustdiag  23369  ustinvel  23370  ustexhalf  23371  ust0  23380  imasdsf1olem  23535  tngngp3  23829  lmhmclm  24259  iscph  24343  iscau2  24450  pmltpclem1  24621  isi1f  24847  mbfi1fseqlem6  24894  iblcnlem  24962  dvfsumlem4  25202  aannenlem1  25497  aannenlem2  25498  ulmval  25548  istrkgb  26825  istrkge  26827  istrkgld  26829  istrkg2ld  26830  istrkg3ld  26831  axtgupdim2  26841  axtgeucl  26842  trgcgrg  26885  ishlg  26972  colline  27019  iscgra  27179  isinag  27208  brbtwn  27276  axpaschlem  27317  axlowdim  27338  axeuclid  27340  eengtrkge  27364  issubgr  27647  nb3grpr  27758  nb3grpr2  27759  cplgr3v  27811  wksfval  27985  iswlk  27986  upgr2wlk  28045  wlkiswwlks2  28249  wwlksnextfun  28272  wwlksnextinj  28273  wwlksnextbij  28276  wwlksnextprop  28286  2wlkdlem4  28302  umgr2wlk  28323  umgrwwlks2on  28331  elwspths2spth  28341  isclwwlk  28357  clwlkclwwlklem1  28372  erclwwlkeq  28391  clwwlkn1loopb  28416  erclwwlkneq  28440  s2elclwwlknon2  28477  3wlkdlem5  28536  3wlkdlem6  28538  3wlkdlem9  28541  3wlkdlem10  28542  uhgr3cyclex  28555  upgr4cycl4dv4e  28558  frgr3v  28648  3cyclfrgrrn1  28658  extwwlkfabel  28726  isplig  28847  lpni  28851  isgrpo  28868  vciOLD  28932  isvclem  28948  isnvlem  28981  sspval  29094  isssp  29095  ajfval  29180  dipdir  29213  siilem2  29223  issh  29579  elunop2  30384  superpos  30725  padct  31063  resspos  31253  isslmd  31464  slmdlema  31465  elrspunidl  31615  locfinreflem  31799  locfinref  31800  zarcmplem  31840  zhmnrg  31926  ismntoplly  31984  issiga  32089  isrnsiga  32090  isldsys  32133  rossros  32157  ismeas  32176  isrnmeas  32177  pmeasmono  32300  pmeasadd  32301  istrkg2d  32655  axtgupdim2ALTV  32657  afsval  32660  brafs  32661  bnj919  32756  bnj976  32766  bnj607  32905  bnj873  32913  cvmlift3lem2  33291  cvmlift3lem6  33295  cvmlift3lem7  33296  cvmlift3lem9  33298  cvmlift3  33299  mclsppslem  33554  dfon2lem1  33768  dfon2lem3  33770  dfon2lem7  33774  xpord2lem  33798  poxp2  33799  xpord3lem  33804  xpord3pred  33807  on2ind  33837  on3ind  33838  nodense  33904  nosupprefixmo  33912  noinfprefixmo  33913  nosupcbv  33914  nosupfv  33918  noinfcbv  33929  noinffv  33933  noetalem2  33954  eqscut  34008  no2indslem  34120  no3inds  34124  brofs  34316  ofscom  34318  btwnouttr  34335  brifs  34354  cgr3com  34364  brcolinear  34370  brfs  34390  unblimceq0lem  34695  knoppndvlem21  34721  rdgeqoa  35550  poimirlem4  35790  poimirlem27  35813  mblfinlem3  35825  indexa  35900  sdclem1  35910  fdc  35912  neificl  35920  heiborlem2  35979  isass  36013  ismndo2  36041  isrngo  36064  rngomndo  36102  isgrpda  36122  igenval2  36233  eleqvrels2  36712  eleqvrels3  36713  eqvreleq  36722  lshpset2N  37140  isopos  37201  oposlem  37203  cmtfvalN  37231  cvrfval  37289  3dimlem1  37479  3dim1lem5  37487  lplni2  37558  lvoli2  37602  4atlem11  37630  dalawlem15  37906  cdlemftr3  38586  tendofset  38779  tendoset  38780  istendo  38781  cdlemk28-3  38929  cdlemkid3N  38954  cdlemkid4  38955  lpolsetN  39503  islpolN  39504  lpolconN  39508  ismrc  40530  rabren3dioph  40644  irrapxlem5  40655  rmydioph  40843  mpaaeu  40982  mpaaval  40983  mpaalem  40984  dfsucon  41137  minregex  41148  dfrtrcl3  41348  brco3f1o  41650  grumnud  41911  eliooshift  43051  stoweidlem5  43553  stoweidlem18  43566  stoweidlem28  43576  stoweidlem31  43579  stoweidlem41  43589  stoweidlem43  43591  stoweidlem44  43592  stoweidlem45  43593  stoweidlem51  43599  stoweidlem55  43603  stoweidlem59  43607  issal  43862  fundcmpsurbijinjpreimafv  44870  fundcmpsurbijinj  44873  fundcmpsurinjALT  44875  ichnreuop  44935  proththdlem  45076  6gbe  45234  8gbe  45236  bgoldbtbndlem2  45269  bgoldbtbndlem3  45270  bgoldbtbnd  45272  upwlksfval  45308  isupwlk  45309  el0ldep  45818  ldepspr  45825  lmod1  45844  zlmodzxzldep  45856  catprs  46303  catprsc  46305  prsthinc  46346