Theorem 3anbi123d 1465

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3anbi12d  1466  3anbi13d  1467  3anbi23d  1468  ax12wdemo  2174  limeq  6400  f13dfv  7313  epne3  7819  oteqimp  8054  xpord2lem  8196  poxp2  8197  xpord3lem  8203  xpord3pred  8206  csbfrecsg  8340  frrlem1  8342  frrlem13  8354  smoeq  8396  on2ind  8716  on3ind  8717  naddasslem1  8742  naddasslem2  8743  naddass  8744  ereq1  8763  sbthfi  9252  indexfi  9387  hartogslem1  9573  brttrcl2  9752  ssttrcl  9753  ttrcltr  9754  ttrclss  9758  ttrclselem2  9764  tz9.1  9767  updjud  10052  alephval3  10228  cofsmo  10386  cfsmolem  10387  alephsing  10393  axdc3lem2  10568  axdc3lem3  10569  axdc3  10571  axdc4lem  10572  zornn0g  10622  fpwwe2lem4  10758  canthwelem  10774  canthwe  10775  pwfseqlem4a  10785  pwfseqlem4  10786  elwina  10810  elina  10811  iswun  10828  elgrug  10916  iccshftr  13657  iccshftl  13659  iccdil  13661  icccntr  13663  fzaddel  13732  elfzomelpfzo  13947  axdc4uzlem  14166  hash3tpb  14681  wrdl1s1  14804  wwlktovf  15152  wwlktovf1  15153  wwlktovfo  15154  wrd2f1tovbij  15156  dfrtrcl2  15258  sqrmo  15461  resqrtcl  15463  resqrtthlem  15464  sqrtneg  15477  sqreu  15572  sqrtthlem  15574  eqsqrtd  15579  prodeq1f  16119  prodeq1  16120  zprod  16148  divalglem10  16616  dfgcd2  16763  coprmprod  16880  pythagtriplem18  17054  pythagtriplem19  17055  prmgaplem3  17275  prmgaplem4  17276  isstruct2  17371  imasval  17733  mreexexlemd  17868  catidd  17904  iscatd2  17905  subsubc  18078  isfunc  18089  funcres2b  18122  ispos  18538  posi  18541  isposd  18546  pospropd  18549  resspos  18653  isps  18792  imasmnd2  19018  sgrp2rid2ex  19176  imasgrp2  19315  psgnunilem3  19761  isrngd  20446  imasrng  20450  isringd  20573  imasring  20611  subrngpropd  20871  isdrngd  21073  isdrngdOLD  21075  islmod  21190  lmodlema  21191  islmodd  21192  lmodprop2d  21250  lmhmpropd  21399  rspprop  21575  isphl  21989  isphld  22015  phlpropd  22016  mdetunilem3  22984  mdetunilem9  22990  fiinopn  23274  iscldtop  23468  lmfval  23605  connsuba  23793  1stcfb  23818  2ndcctbss  23829  subislly  23855  ptval  23944  elpt  23946  elptr  23947  upxp  23997  isfbas  24203  ustval  24577  isust  24578  ustincl  24582  ustdiag  24583  ustinvel  24584  ustexhalf  24585  ust0  24594  imasdsf1olem  24747  tngngp3  25030  lmhmclm  25463  iscph  25546  iscau2  25653  pmltpclem1  25824  isi1f  26050  mbfi1fseqlem6  26096  iblcnlem  26164  dvfsumlem4  26404  aannenlem1  26712  aannenlem2  26713  ulmval  26764  nodense  28106  nosupprefixmo  28114  noinfprefixmo  28115  nosupcbv  28116  nosupfv  28120  noinfcbv  28131  noinffv  28135  noetalem2  28156  eqcuts  28228  no2indlesm  28397  no3inds  28401  addsproplem3  28414  negsproplem3  28473  mulsproplem10  28568  bdayfinbndcbv  28909  bdayfinbndlem1  28910  bdayfinbndlem2  28911  istrkgb  28974  istrkge  28976  istrkgld  28978  istrkg2ld  28979  istrkg3ld  28980  axtgupdim2  28990  axtgeucl  28991  trgcgrg  29035  ishlg2  29122  ishlg  29125  colline  29175  iscgra  29373  isinag  29414  cgrabasimass  29435  angmgmaddov1  29445  angmgmaddcl  29448  angmgmval  29451  brbtwn  29534  axpaschlem  29575  axlowdim  29596  axeuclid  29598  eengtrkge  29622  issubgr  29909  nb3grpr  30020  nb3grpr2  30021  cplgr3v  30073  wksfval  30247  iswlk  30248  upgr2wlk  30304  wlkiswwlks2  30521  wwlksnextfun  30544  wwlksnextinj  30545  wwlksnextbij  30548  wwlksnextprop  30558  2wlkdlem4  30574  umgr2wlk  30595  usgrwwlks2on  30604  umgrwwlks2on  30605  elwspths2spth  30616  isclwwlk  30632  clwlkclwwlklem1  30647  erclwwlkeq  30666  clwwlkn1loopb  30691  erclwwlkneq  30715  s2elclwwlknon2  30752  3wlkdlem5  30821  3wlkdlem6  30823  3wlkdlem9  30826  3wlkdlem10  30827  uhgr3cyclex  30840  upgr4cycl4dv4e  30843  frgr3v  30933  3cyclfrgrrn1  30943  extwwlkfabel  31011  isplig  31135  lpni  31139  isgrpo  31156  vciOLD  31220  isvclem  31236  isnvlem  31269  sspval  31382  isssp  31383  ajfval  31468  dipdir  31501  siilem2  31511  issh  31867  elunop2  32672  superpos  33013  padct  33407  isslmd  33862  slmdlema  33863  subsdrg  33964  elrspunidl  34082  constrcbvlem  34498  locfinreflem  34583  locfinref  34584  zarcmplem  34624  zhmnrg  34708  ismntoplly  34768  issiga  34855  isrnsiga  34856  isldsys  34900  rossros  34924  ismeas  34943  isrnmeas  34944  pmeasmono  35067  pmeasadd  35068  istrkg2d  35406  axtgupdim2ALTV  35408  afsval  35414  brafs  35415  bnj919  35509  bnj976  35519  bnj607  35657  bnj873  35665  weexenwe  35889  fineqvnttrclse  35933  tz9.1regs  35943  onprcf1acwevdlem1  36086  srepdflem2  36127  srepdf  36128  cvmlift3lem2  36293  cvmlift3lem6  36297  cvmlift3lem7  36298  cvmlift3lem9  36300  cvmlift3  36301  mclsppslem  36556  mirimanoffr  36668  dfon2lem3  36762  dfon2lem7  36766  brofs  36985  ofscom  36987  btwnouttr  37004  brifs  37023  cgr3com  37033  brcolinear  37039  brfs  37059  prodeq12sdv  37222  cbvproddavw2  37300  unblimceq0lem  37587  knoppndvlem21  37613  rdgeqoa  38561  poimirlem4  38810  poimirlem27  38833  mblfinlem3  38845  indexa  38935  sdclem1  38943  fdc  38945  neificl  38953  heiborlem2  39012  isass  39046  ismndo2  39074  isrngo  39097  rngomndo  39135  isgrpda  39155  igenval2  39266  eleqvrels2  39874  eleqvrels3  39875  eqvreleq  39884  lshpset2N  40442  isopos  40503  oposlem  40505  cmtfvalN  40533  cvrfval  40591  3dimlem1  40781  3dim1lem5  40789  lplni2  40860  lvoli2  40904  4atlem11  40932  dalawlem15  41208  cdlemftr3  41888  tendofset  42081  tendoset  42082  istendo  42083  cdlemk28-3  42231  cdlemkid3N  42256  cdlemkid4  42257  lpolsetN  42805  islpolN  42806  lpolconN  42810  isprimroot  43409  aks6d1c1p1  43423  ismrc  43978  rabren3dioph  44088  irrapxlem5  44099  rmydioph  44287  mpaaeu  44417  mpaaval  44418  mpaalem  44419  naddwordnexlem4  44664  dfsucon  44785  minregex  44796  dfrtrcl3  44994  brco3f1o  45294  grumnud  45531  modelaxreplem1  46232  modelaxreplem2  46233  modelaxrep  46235  eliooshift  46791  stoweidlem5  47288  stoweidlem18  47301  stoweidlem28  47311  stoweidlem31  47314  stoweidlem41  47324  stoweidlem43  47326  stoweidlem44  47327  stoweidlem45  47328  stoweidlem51  47334  stoweidlem55  47338  stoweidlem59  47342  issal  47597  fundcmpsurbijinjpreimafv  48762  fundcmpsurbijinj  48765  fundcmpsurinjALT  48767  ichnreuop  48827  proththdlem  48971  6gbe  49142  8gbe  49144  bgoldbtbndlem2  49177  bgoldbtbndlem3  49178  bgoldbtbnd  49180  grtriproplem  49310  grtri  49311  grtrif1o  49313  isgrtri  49314  grimgrtri  49320  usgrexmpl1tri  49396  gpgvtx0  49424  gpgvtx1  49425  gpgedgvtx0  49432  gpgedgvtx1  49433  upwlksfval  49506  isupwlk  49507  el0ldep  49909  ldepspr  49916  lmod1  49935  zlmodzxzldep  49947  catprs  50456  catprsc  50458  prsthinc  50930  2arwcatlem1  51064  cnelsubcw  51072