Theorem 3anbi123d 1456

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  3anbi12d  1457  3anbi13d  1458  3anbi23d  1459  ax12wdemo  2168  limeq  6353  f13dfv  7253  epne3  7751  oteqimp  7984  xpord2lem  8116  poxp2  8117  xpord3lem  8123  xpord3pred  8126  csbfrecsg  8259  frrlem1  8261  frrlem13  8273  smoeq  8315  on2ind  8633  on3ind  8634  naddasslem1  8659  naddasslem2  8660  naddass  8661  ereq1  8680  sbthfi  9161  indexfi  9297  hartogslem1  9484  brttrcl2  9663  ssttrcl  9664  ttrcltr  9665  ttrclss  9669  ttrclselem2  9675  tz9.1  9678  updjud  9886  alephval3  10060  cofsmo  10220  cfsmolem  10221  alephsing  10227  axdc3lem2  10402  axdc3lem3  10403  axdc3  10405  axdc4lem  10406  zornn0g  10456  fpwwe2lem4  10586  canthwelem  10602  canthwe  10603  pwfseqlem4a  10613  pwfseqlem4  10614  elwina  10638  elina  10639  iswun  10656  elgrug  10744  iccshftr  13484  iccshftl  13486  iccdil  13488  icccntr  13490  fzaddel  13557  elfzomelpfzo  13772  axdc4uzlem  13990  hash3tpb  14502  wrdl1s1  14622  wwlktovf  14963  wwlktovf1  14964  wwlktovfo  14965  wrd2f1tovbij  14967  dfrtrcl2  15069  sqrmo  15269  resqrtcl  15271  resqrtthlem  15272  sqrtneg  15285  sqreu  15379  sqrtthlem  15381  eqsqrtd  15386  prodeq1f  15927  prodeq1  15928  zprod  15958  divalglem10  16427  dfgcd2  16571  coprmprod  16686  pythagtriplem18  16859  pythagtriplem19  16860  prmgaplem3  17080  prmgaplem4  17081  isstruct2  17176  imasval  17532  mreexexlemd  17667  catidd  17703  iscatd2  17704  subsubc  17877  isfunc  17888  funcres2b  17921  ispos  18337  posi  18340  isposd  18345  pospropd  18348  resspos  18452  isps  18591  imasmnd2  18799  sgrp2rid2ex  18955  imasgrp2  19088  psgnunilem3  19527  isrngd  20210  imasrng  20214  isringd  20328  imasring  20366  subrngpropd  20605  isdrngd  20802  isdrngdOLD  20804  islmod  20919  lmodlema  20920  islmodd  20921  lmodprop2d  20979  lmhmpropd  21128  isphl  21668  isphld  21694  phlpropd  21695  mdetunilem3  22662  mdetunilem9  22668  fiinopn  22949  iscldtop  23143  lmfval  23280  connsuba  23468  1stcfb  23493  2ndcctbss  23503  subislly  23529  ptval  23618  elpt  23620  elptr  23621  upxp  23671  isfbas  23877  ustval  24251  isust  24252  ustincl  24256  ustdiag  24257  ustinvel  24258  ustexhalf  24259  ust0  24268  imasdsf1olem  24421  tngngp3  24704  lmhmclm  25137  iscph  25220  iscau2  25327  pmltpclem1  25498  isi1f  25724  mbfi1fseqlem6  25770  iblcnlem  25839  dvfsumlem4  26079  aannenlem1  26380  aannenlem2  26381  ulmval  26431  nodense  27744  nosupprefixmo  27752  noinfprefixmo  27753  nosupcbv  27754  nosupfv  27758  noinfcbv  27769  noinffv  27773  noetalem2  27794  eqcuts  27866  no2indlesm  28035  no3inds  28039  addsproplem3  28052  negsproplem3  28111  mulsproplem10  28206  bdayfinbndcbv  28547  bdayfinbndlem1  28548  bdayfinbndlem2  28549  istrkgb  28612  istrkge  28614  istrkgld  28616  istrkg2ld  28617  istrkg3ld  28618  axtgupdim2  28628  axtgeucl  28629  trgcgrg  28672  ishlg  28759  colline  28806  iscgra  28966  isinag  28995  brbtwn  29057  axpaschlem  29098  axlowdim  29119  axeuclid  29121  eengtrkge  29145  issubgr  29429  nb3grpr  29540  nb3grpr2  29541  cplgr3v  29593  wksfval  29767  iswlk  29768  upgr2wlk  29824  wlkiswwlks2  30032  wwlksnextfun  30055  wwlksnextinj  30056  wwlksnextbij  30059  wwlksnextprop  30069  2wlkdlem4  30085  umgr2wlk  30106  usgrwwlks2on  30115  umgrwwlks2on  30116  elwspths2spth  30127  isclwwlk  30143  clwlkclwwlklem1  30158  erclwwlkeq  30177  clwwlkn1loopb  30202  erclwwlkneq  30226  s2elclwwlknon2  30263  3wlkdlem5  30322  3wlkdlem6  30324  3wlkdlem9  30327  3wlkdlem10  30328  uhgr3cyclex  30341  upgr4cycl4dv4e  30344  frgr3v  30434  3cyclfrgrrn1  30444  extwwlkfabel  30512  isplig  30636  lpni  30640  isgrpo  30657  vciOLD  30721  isvclem  30737  isnvlem  30770  sspval  30883  isssp  30884  ajfval  30969  dipdir  31002  siilem2  31012  issh  31368  elunop2  32173  superpos  32514  padct  32881  isslmd  33343  slmdlema  33344  subsdrg  33446  elrspunidl  33575  constrcbvlem  34013  locfinreflem  34098  locfinref  34099  zarcmplem  34139  zhmnrg  34223  ismntoplly  34283  issiga  34370  isrnsiga  34371  isldsys  34414  rossros  34438  ismeas  34457  isrnmeas  34458  pmeasmono  34582  pmeasadd  34583  istrkg2d  34921  axtgupdim2ALTV  34923  afsval  34929  brafs  34930  bnj919  35024  bnj976  35034  bnj607  35172  bnj873  35180  fineqvnttrclse  35381  tz9.1regs  35391  cvmlift3lem2  35631  cvmlift3lem6  35635  cvmlift3lem7  35636  cvmlift3lem9  35638  cvmlift3  35639  mclsppslem  35894  dfon2lem1  36092  dfon2lem3  36094  dfon2lem7  36098  brofs  36316  ofscom  36318  btwnouttr  36335  brifs  36354  cgr3com  36364  brcolinear  36370  brfs  36390  prodeq12sdv  36539  cbvproddavw2  36617  unblimceq0lem  36905  knoppndvlem21  36931  rdgeqoa  37825  poimirlem4  38084  poimirlem27  38107  mblfinlem3  38119  indexa  38193  sdclem1  38203  fdc  38205  neificl  38213  heiborlem2  38272  isass  38306  ismndo2  38334  isrngo  38357  rngomndo  38395  isgrpda  38415  igenval2  38526  eleqvrels2  39136  eleqvrels3  39137  eqvreleq  39146  lshpset2N  39704  isopos  39765  oposlem  39767  cmtfvalN  39795  cvrfval  39853  3dimlem1  40043  3dim1lem5  40051  lplni2  40122  lvoli2  40166  4atlem11  40194  dalawlem15  40470  cdlemftr3  41150  tendofset  41343  tendoset  41344  istendo  41345  cdlemk28-3  41493  cdlemkid3N  41518  cdlemkid4  41519  lpolsetN  42067  islpolN  42068  lpolconN  42072  isprimroot  42671  aks6d1c1p1  42685  ismrc  43243  rabren3dioph  43353  irrapxlem5  43364  rmydioph  43552  mpaaeu  43688  mpaaval  43689  mpaalem  43690  naddwordnexlem4  43939  dfsucon  44060  minregex  44071  dfrtrcl3  44270  brco3f1o  44570  grumnud  44823  modelaxreplem1  45515  modelaxreplem2  45516  modelaxrep  45518  eliooshift  46043  stoweidlem5  46540  stoweidlem18  46553  stoweidlem28  46563  stoweidlem31  46566  stoweidlem41  46576  stoweidlem43  46578  stoweidlem44  46579  stoweidlem45  46580  stoweidlem51  46586  stoweidlem55  46590  stoweidlem59  46594  issal  46849  fundcmpsurbijinjpreimafv  47974  fundcmpsurbijinj  47977  fundcmpsurinjALT  47979  ichnreuop  48039  proththdlem  48183  6gbe  48354  8gbe  48356  bgoldbtbndlem2  48389  bgoldbtbndlem3  48390  bgoldbtbnd  48392  grtriproplem  48522  grtri  48523  grtrif1o  48525  isgrtri  48526  grimgrtri  48532  usgrexmpl1tri  48608  gpgvtx0  48636  gpgvtx1  48637  gpgedgvtx0  48644  gpgedgvtx1  48645  upwlksfval  48718  isupwlk  48719  el0ldep  49049  ldepspr  49056  lmod1  49075  zlmodzxzldep  49087  catprs  49593  catprsc  49595  prsthinc  50046  2arwcatlem1  50177  cnelsubclem  50185