Theorem 3anbi123d 1464

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  1465  3anbi13d  1466  3anbi23d  1467  ax12wdemo  2172  limeq  6369  f13dfv  7275  epne3  7772  oteqimp  8005  xpord2lem  8140  poxp2  8141  xpord3lem  8147  xpord3pred  8150  csbfrecsg  8283  frrlem1  8285  frrlem13  8297  smoeq  8339  on2ind  8657  on3ind  8658  naddasslem1  8683  naddasslem2  8684  naddass  8685  ereq1  8704  sbthfi  9193  indexfi  9327  hartogslem1  9514  brttrcl2  9693  ssttrcl  9694  ttrcltr  9695  ttrclss  9699  ttrclselem2  9705  tz9.1  9708  updjud  9939  alephval3  10113  cofsmo  10271  cfsmolem  10272  alephsing  10278  axdc3lem2  10453  axdc3lem3  10454  axdc3  10456  axdc4lem  10457  zornn0g  10507  fpwwe2lem4  10643  canthwelem  10659  canthwe  10660  pwfseqlem4a  10670  pwfseqlem4  10671  elwina  10695  elina  10696  iswun  10713  elgrug  10801  iccshftr  13539  iccshftl  13541  iccdil  13543  icccntr  13545  fzaddel  13613  elfzomelpfzo  13828  axdc4uzlem  14047  hash3tpb  14560  wrdl1s1  14682  wwlktovf  15029  wwlktovf1  15030  wwlktovfo  15031  wrd2f1tovbij  15033  dfrtrcl2  15135  sqrmo  15338  resqrtcl  15340  resqrtthlem  15341  sqrtneg  15354  sqreu  15448  sqrtthlem  15450  eqsqrtd  15455  prodeq1f  15995  prodeq1  15996  zprod  16024  divalglem10  16492  dfgcd2  16636  coprmprod  16751  pythagtriplem18  16924  pythagtriplem19  16925  prmgaplem3  17145  prmgaplem4  17146  isstruct2  17241  imasval  17597  mreexexlemd  17732  catidd  17768  iscatd2  17769  subsubc  17942  isfunc  17953  funcres2b  17986  ispos  18402  posi  18405  isposd  18410  pospropd  18413  resspos  18517  isps  18656  imasmnd2  18881  sgrp2rid2ex  19039  imasgrp2  19178  psgnunilem3  19623  isrngd  20308  imasrng  20312  isringd  20433  imasring  20471  subrngpropd  20730  isdrngd  20931  isdrngdOLD  20933  islmod  21048  lmodlema  21049  islmodd  21050  lmodprop2d  21108  lmhmpropd  21257  rspprop  21433  isphl  21841  isphld  21867  phlpropd  21868  mdetunilem3  22836  mdetunilem9  22842  fiinopn  23126  iscldtop  23320  lmfval  23457  connsuba  23645  1stcfb  23670  2ndcctbss  23681  subislly  23707  ptval  23796  elpt  23798  elptr  23799  upxp  23849  isfbas  24055  ustval  24429  isust  24430  ustincl  24434  ustdiag  24435  ustinvel  24436  ustexhalf  24437  ust0  24446  imasdsf1olem  24599  tngngp3  24882  lmhmclm  25315  iscph  25398  iscau2  25505  pmltpclem1  25676  isi1f  25902  mbfi1fseqlem6  25948  iblcnlem  26016  dvfsumlem4  26256  aannenlem1  26564  aannenlem2  26565  ulmval  26616  nodense  27928  nosupprefixmo  27936  noinfprefixmo  27937  nosupcbv  27938  nosupfv  27942  noinfcbv  27953  noinffv  27957  noetalem2  27978  eqcuts  28050  no2indlesm  28219  no3inds  28223  addsproplem3  28236  negsproplem3  28295  mulsproplem10  28390  bdayfinbndcbv  28731  bdayfinbndlem1  28732  bdayfinbndlem2  28733  istrkgb  28796  istrkge  28798  istrkgld  28800  istrkg2ld  28801  istrkg3ld  28802  axtgupdim2  28812  axtgeucl  28813  trgcgrg  28857  ishlg2  28944  ishlg  28947  colline  28997  iscgra  29195  isinag  29236  cgrabasimass  29257  angmgmaddov1  29267  angmgmaddcl  29270  angmgmval  29273  brbtwn  29356  axpaschlem  29397  axlowdim  29418  axeuclid  29420  eengtrkge  29444  issubgr  29731  nb3grpr  29842  nb3grpr2  29843  cplgr3v  29895  wksfval  30069  iswlk  30070  upgr2wlk  30126  wlkiswwlks2  30343  wwlksnextfun  30366  wwlksnextinj  30367  wwlksnextbij  30370  wwlksnextprop  30380  2wlkdlem4  30396  umgr2wlk  30417  usgrwwlks2on  30426  umgrwwlks2on  30427  elwspths2spth  30438  isclwwlk  30454  clwlkclwwlklem1  30469  erclwwlkeq  30488  clwwlkn1loopb  30513  erclwwlkneq  30537  s2elclwwlknon2  30574  3wlkdlem5  30643  3wlkdlem6  30645  3wlkdlem9  30648  3wlkdlem10  30649  uhgr3cyclex  30662  upgr4cycl4dv4e  30665  frgr3v  30755  3cyclfrgrrn1  30765  extwwlkfabel  30833  isplig  30957  lpni  30961  isgrpo  30978  vciOLD  31042  isvclem  31058  isnvlem  31091  sspval  31204  isssp  31205  ajfval  31290  dipdir  31323  siilem2  31333  issh  31689  elunop2  32494  superpos  32835  padct  33189  isslmd  33642  slmdlema  33643  subsdrg  33739  elrspunidl  33856  constrcbvlem  34265  locfinreflem  34350  locfinref  34351  zarcmplem  34391  zhmnrg  34475  ismntoplly  34535  issiga  34622  isrnsiga  34623  isldsys  34667  rossros  34691  ismeas  34710  isrnmeas  34711  pmeasmono  34835  pmeasadd  34836  istrkg2d  35174  axtgupdim2ALTV  35176  afsval  35182  brafs  35183  bnj919  35277  bnj976  35287  bnj607  35425  bnj873  35433  fineqvnttrclse  35650  tz9.1regs  35660  cvmlift3lem2  35899  cvmlift3lem6  35903  cvmlift3lem7  35904  cvmlift3lem9  35906  cvmlift3  35907  mclsppslem  36162  dfon2lem1  36360  dfon2lem3  36362  dfon2lem7  36366  brofs  36585  ofscom  36587  btwnouttr  36604  brifs  36623  cgr3com  36633  brcolinear  36639  brfs  36659  prodeq12sdv  36838  cbvproddavw2  36916  unblimceq0lem  37203  knoppndvlem21  37229  rdgeqoa  38124  poimirlem4  38373  poimirlem27  38396  mblfinlem3  38408  indexa  38483  sdclem1  38493  fdc  38495  neificl  38503  heiborlem2  38562  isass  38596  ismndo2  38624  isrngo  38647  rngomndo  38685  isgrpda  38705  igenval2  38816  eleqvrels2  39424  eleqvrels3  39425  eqvreleq  39434  lshpset2N  39992  isopos  40053  oposlem  40055  cmtfvalN  40083  cvrfval  40141  3dimlem1  40331  3dim1lem5  40339  lplni2  40410  lvoli2  40454  4atlem11  40482  dalawlem15  40758  cdlemftr3  41438  tendofset  41631  tendoset  41632  istendo  41633  cdlemk28-3  41781  cdlemkid3N  41806  cdlemkid4  41807  lpolsetN  42355  islpolN  42356  lpolconN  42360  isprimroot  42959  aks6d1c1p1  42973  ismrc  43546  rabren3dioph  43656  irrapxlem5  43667  rmydioph  43855  mpaaeu  43991  mpaaval  43992  mpaalem  43993  naddwordnexlem4  44242  dfsucon  44363  minregex  44374  dfrtrcl3  44573  brco3f1o  44873  grumnud  45110  modelaxreplem1  45801  modelaxreplem2  45802  modelaxrep  45804  eliooshift  46336  stoweidlem5  46833  stoweidlem18  46846  stoweidlem28  46856  stoweidlem31  46859  stoweidlem41  46869  stoweidlem43  46871  stoweidlem44  46872  stoweidlem45  46873  stoweidlem51  46879  stoweidlem55  46883  stoweidlem59  46887  issal  47142  fundcmpsurbijinjpreimafv  48307  fundcmpsurbijinj  48310  fundcmpsurinjALT  48312  ichnreuop  48372  proththdlem  48516  6gbe  48687  8gbe  48689  bgoldbtbndlem2  48722  bgoldbtbndlem3  48723  bgoldbtbnd  48725  grtriproplem  48855  grtri  48856  grtrif1o  48858  isgrtri  48859  grimgrtri  48865  usgrexmpl1tri  48941  gpgvtx0  48969  gpgvtx1  48970  gpgedgvtx0  48977  gpgedgvtx1  48978  upwlksfval  49051  isupwlk  49052  el0ldep  49396  ldepspr  49403  lmod1  49422  zlmodzxzldep  49434  catprs  49937  catprsc  49939  prsthinc  50390  2arwcatlem1  50521  cnelsubclem  50529