Theorem 3anbi123d 1439

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 633	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜃) ↔ (𝜒 ∧ 𝜏)))
4		bi3d.3	. . 3 ⊢ (𝜑 → (𝜂 ↔ 𝜁))
5	3, 4	anbi12d 633	. 2 ⊢ (𝜑 → (((𝜓 ∧ 𝜃) ∧ 𝜂) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁)))
6		df-3an 1089	. 2 ⊢ ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ ((𝜓 ∧ 𝜃) ∧ 𝜂))
7		df-3an 1089	. 2 ⊢ ((𝜒 ∧ 𝜏 ∧ 𝜁) ↔ ((𝜒 ∧ 𝜏) ∧ 𝜁))
8	5, 6, 7	3bitr4g 314	1 ⊢ (𝜑 → ((𝜓 ∧ 𝜃 ∧ 𝜂) ↔ (𝜒 ∧ 𝜏 ∧ 𝜁)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  3anbi12d  1440  3anbi13d  1441  3anbi23d  1442  ax12wdemo  2141  limeq  6329  f13dfv  7222  epne3  7720  oteqimp  7954  xpord2lem  8085  poxp2  8086  xpord3lem  8092  xpord3pred  8095  csbfrecsg  8227  frrlem1  8229  frrlem13  8241  smoeq  8283  on2ind  8598  on3ind  8599  naddasslem1  8623  naddasslem2  8624  naddass  8625  ereq1  8644  sbthfi  9126  indexfi  9263  hartogslem1  9450  brttrcl2  9626  ssttrcl  9627  ttrcltr  9628  ttrclss  9632  ttrclselem2  9638  tz9.1  9641  updjud  9849  alephval3  10023  cofsmo  10182  cfsmolem  10183  alephsing  10189  axdc3lem2  10364  axdc3lem3  10365  axdc3  10367  axdc4lem  10368  zornn0g  10418  fpwwe2lem4  10548  canthwelem  10564  canthwe  10565  pwfseqlem4a  10575  pwfseqlem4  10576  elwina  10600  elina  10601  iswun  10618  elgrug  10706  iccshftr  13430  iccshftl  13432  iccdil  13434  icccntr  13436  fzaddel  13503  elfzomelpfzo  13718  axdc4uzlem  13936  hash3tpb  14448  wrdl1s1  14568  wwlktovf  14909  wwlktovf1  14910  wwlktovfo  14911  wrd2f1tovbij  14913  dfrtrcl2  15015  sqrmo  15204  resqrtcl  15206  resqrtthlem  15207  sqrtneg  15220  sqreu  15314  sqrtthlem  15316  eqsqrtd  15321  prodeq1f  15862  prodeq1  15863  zprod  15893  divalglem10  16362  dfgcd2  16506  coprmprod  16621  pythagtriplem18  16794  pythagtriplem19  16795  prmgaplem3  17015  prmgaplem4  17016  isstruct2  17110  imasval  17466  mreexexlemd  17601  catidd  17637  iscatd2  17638  subsubc  17811  isfunc  17822  funcres2b  17855  ispos  18271  posi  18274  isposd  18279  pospropd  18282  resspos  18386  isps  18525  imasmnd2  18733  sgrp2rid2ex  18889  imasgrp2  19022  psgnunilem3  19462  isrngd  20145  imasrng  20149  isringd  20263  imasring  20301  subrngpropd  20536  isdrngd  20733  isdrngdOLD  20735  islmod  20850  lmodlema  20851  islmodd  20852  lmodprop2d  20910  lmhmpropd  21060  isphl  21618  isphld  21644  phlpropd  21645  mdetunilem3  22589  mdetunilem9  22595  fiinopn  22876  iscldtop  23070  lmfval  23207  connsuba  23395  1stcfb  23420  2ndcctbss  23430  subislly  23456  ptval  23545  elpt  23547  elptr  23548  upxp  23598  isfbas  23804  ustval  24178  isust  24179  ustincl  24183  ustdiag  24184  ustinvel  24185  ustexhalf  24186  ust0  24195  imasdsf1olem  24348  tngngp3  24631  lmhmclm  25064  iscph  25147  iscau2  25254  pmltpclem1  25425  isi1f  25651  mbfi1fseqlem6  25697  iblcnlem  25766  dvfsumlem4  26006  aannenlem1  26305  aannenlem2  26306  ulmval  26358  nodense  27670  nosupprefixmo  27678  noinfprefixmo  27679  nosupcbv  27680  nosupfv  27684  noinfcbv  27695  noinffv  27699  noetalem2  27720  eqcuts  27791  no2indlesm  27960  no3inds  27964  addsproplem3  27977  negsproplem3  28036  mulsproplem10  28131  bdayfinbndcbv  28472  bdayfinbndlem1  28473  bdayfinbndlem2  28474  istrkgb  28537  istrkge  28539  istrkgld  28541  istrkg2ld  28542  istrkg3ld  28543  axtgupdim2  28553  axtgeucl  28554  trgcgrg  28597  ishlg  28684  colline  28731  iscgra  28891  isinag  28920  brbtwn  28982  axpaschlem  29023  axlowdim  29044  axeuclid  29046  eengtrkge  29070  issubgr  29354  nb3grpr  29465  nb3grpr2  29466  cplgr3v  29518  wksfval  29693  iswlk  29694  upgr2wlk  29750  wlkiswwlks2  29958  wwlksnextfun  29981  wwlksnextinj  29982  wwlksnextbij  29985  wwlksnextprop  29995  2wlkdlem4  30011  umgr2wlk  30032  usgrwwlks2on  30041  umgrwwlks2on  30042  elwspths2spth  30053  isclwwlk  30069  clwlkclwwlklem1  30084  erclwwlkeq  30103  clwwlkn1loopb  30128  erclwwlkneq  30152  s2elclwwlknon2  30189  3wlkdlem5  30248  3wlkdlem6  30250  3wlkdlem9  30253  3wlkdlem10  30254  uhgr3cyclex  30267  upgr4cycl4dv4e  30270  frgr3v  30360  3cyclfrgrrn1  30370  extwwlkfabel  30438  isplig  30562  lpni  30566  isgrpo  30583  vciOLD  30647  isvclem  30663  isnvlem  30696  sspval  30809  isssp  30810  ajfval  30895  dipdir  30928  siilem2  30938  issh  31294  elunop2  32099  superpos  32440  padct  32806  isslmd  33278  slmdlema  33279  subsdrg  33374  elrspunidl  33503  constrcbvlem  33915  locfinreflem  34000  locfinref  34001  zarcmplem  34041  zhmnrg  34125  ismntoplly  34185  issiga  34272  isrnsiga  34273  isldsys  34316  rossros  34340  ismeas  34359  isrnmeas  34360  pmeasmono  34484  pmeasadd  34485  istrkg2d  34826  axtgupdim2ALTV  34828  afsval  34831  brafs  34832  bnj919  34926  bnj976  34936  bnj607  35074  bnj873  35082  fineqvnttrclse  35284  tz9.1regs  35294  cvmlift3lem2  35518  cvmlift3lem6  35522  cvmlift3lem7  35523  cvmlift3lem9  35525  cvmlift3  35526  mclsppslem  35781  dfon2lem1  35979  dfon2lem3  35981  dfon2lem7  35985  brofs  36203  ofscom  36205  btwnouttr  36222  brifs  36241  cgr3com  36251  brcolinear  36257  brfs  36277  prodeq12sdv  36416  cbvproddavw2  36494  unblimceq0lem  36782  knoppndvlem21  36808  rdgeqoa  37700  poimirlem4  37959  poimirlem27  37982  mblfinlem3  37994  indexa  38068  sdclem1  38078  fdc  38080  neificl  38088  heiborlem2  38147  isass  38181  ismndo2  38209  isrngo  38232  rngomndo  38270  isgrpda  38290  igenval2  38401  eleqvrels2  39011  eleqvrels3  39012  eqvreleq  39021  lshpset2N  39579  isopos  39640  oposlem  39642  cmtfvalN  39670  cvrfval  39728  3dimlem1  39918  3dim1lem5  39926  lplni2  39997  lvoli2  40041  4atlem11  40069  dalawlem15  40345  cdlemftr3  41025  tendofset  41218  tendoset  41219  istendo  41220  cdlemk28-3  41368  cdlemkid3N  41393  cdlemkid4  41394  lpolsetN  41942  islpolN  41943  lpolconN  41947  isprimroot  42546  aks6d1c1p1  42560  ismrc  43147  rabren3dioph  43261  irrapxlem5  43272  rmydioph  43460  mpaaeu  43596  mpaaval  43597  mpaalem  43598  naddwordnexlem4  43847  dfsucon  43968  minregex  43979  dfrtrcl3  44178  brco3f1o  44478  grumnud  44731  modelaxreplem1  45423  modelaxreplem2  45424  modelaxrep  45426  eliooshift  45954  stoweidlem5  46451  stoweidlem18  46464  stoweidlem28  46474  stoweidlem31  46477  stoweidlem41  46487  stoweidlem43  46489  stoweidlem44  46490  stoweidlem45  46491  stoweidlem51  46497  stoweidlem55  46501  stoweidlem59  46505  issal  46760  fundcmpsurbijinjpreimafv  47879  fundcmpsurbijinj  47882  fundcmpsurinjALT  47884  ichnreuop  47944  proththdlem  48088  6gbe  48259  8gbe  48261  bgoldbtbndlem2  48294  bgoldbtbndlem3  48295  bgoldbtbnd  48297  grtriproplem  48427  grtri  48428  grtrif1o  48430  isgrtri  48431  grimgrtri  48437  usgrexmpl1tri  48513  gpgvtx0  48541  gpgvtx1  48542  gpgedgvtx0  48549  gpgedgvtx1  48550  upwlksfval  48623  isupwlk  48624  el0ldep  48954  ldepspr  48961  lmod1  48980  zlmodzxzldep  48992  catprs  49498  catprsc  49500  prsthinc  49951  2arwcatlem1  50082  cnelsubclem  50090