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  6335  f13dfv  7229  epne3  7727  oteqimp  7961  xpord2lem  8092  poxp2  8093  xpord3lem  8099  xpord3pred  8102  csbfrecsg  8234  frrlem1  8236  frrlem13  8248  smoeq  8290  on2ind  8605  on3ind  8606  naddasslem1  8630  naddasslem2  8631  naddass  8632  ereq1  8651  sbthfi  9133  indexfi  9270  hartogslem1  9457  brttrcl2  9635  ssttrcl  9636  ttrcltr  9637  ttrclss  9641  ttrclselem2  9647  tz9.1  9650  updjud  9858  alephval3  10032  cofsmo  10191  cfsmolem  10192  alephsing  10198  axdc3lem2  10373  axdc3lem3  10374  axdc3  10376  axdc4lem  10377  zornn0g  10427  fpwwe2lem4  10557  canthwelem  10573  canthwe  10574  pwfseqlem4a  10584  pwfseqlem4  10585  elwina  10609  elina  10610  iswun  10627  elgrug  10715  iccshftr  13439  iccshftl  13441  iccdil  13443  icccntr  13445  fzaddel  13512  elfzomelpfzo  13727  axdc4uzlem  13945  hash3tpb  14457  wrdl1s1  14577  wwlktovf  14918  wwlktovf1  14919  wwlktovfo  14920  wrd2f1tovbij  14922  dfrtrcl2  15024  sqrmo  15213  resqrtcl  15215  resqrtthlem  15216  sqrtneg  15229  sqreu  15323  sqrtthlem  15325  eqsqrtd  15330  prodeq1f  15871  prodeq1  15872  zprod  15902  divalglem10  16371  dfgcd2  16515  coprmprod  16630  pythagtriplem18  16803  pythagtriplem19  16804  prmgaplem3  17024  prmgaplem4  17025  isstruct2  17119  imasval  17475  mreexexlemd  17610  catidd  17646  iscatd2  17647  subsubc  17820  isfunc  17831  funcres2b  17864  ispos  18280  posi  18283  isposd  18288  pospropd  18291  resspos  18395  isps  18534  imasmnd2  18742  sgrp2rid2ex  18898  imasgrp2  19031  psgnunilem3  19471  isrngd  20154  imasrng  20158  isringd  20272  imasring  20310  subrngpropd  20545  isdrngd  20742  isdrngdOLD  20744  islmod  20859  lmodlema  20860  islmodd  20861  lmodprop2d  20919  lmhmpropd  21068  isphl  21608  isphld  21634  phlpropd  21635  mdetunilem3  22579  mdetunilem9  22585  fiinopn  22866  iscldtop  23060  lmfval  23197  connsuba  23385  1stcfb  23410  2ndcctbss  23420  subislly  23446  ptval  23535  elpt  23537  elptr  23538  upxp  23588  isfbas  23794  ustval  24168  isust  24169  ustincl  24173  ustdiag  24174  ustinvel  24175  ustexhalf  24176  ust0  24185  imasdsf1olem  24338  tngngp3  24621  lmhmclm  25054  iscph  25137  iscau2  25244  pmltpclem1  25415  isi1f  25641  mbfi1fseqlem6  25687  iblcnlem  25756  dvfsumlem4  25996  aannenlem1  26294  aannenlem2  26295  ulmval  26345  nodense  27656  nosupprefixmo  27664  noinfprefixmo  27665  nosupcbv  27666  nosupfv  27670  noinfcbv  27681  noinffv  27685  noetalem2  27706  eqcuts  27777  no2indlesm  27946  no3inds  27950  addsproplem3  27963  negsproplem3  28022  mulsproplem10  28117  bdayfinbndcbv  28458  bdayfinbndlem1  28459  bdayfinbndlem2  28460  istrkgb  28523  istrkge  28525  istrkgld  28527  istrkg2ld  28528  istrkg3ld  28529  axtgupdim2  28539  axtgeucl  28540  trgcgrg  28583  ishlg  28670  colline  28717  iscgra  28877  isinag  28906  brbtwn  28968  axpaschlem  29009  axlowdim  29030  axeuclid  29032  eengtrkge  29056  issubgr  29340  nb3grpr  29451  nb3grpr2  29452  cplgr3v  29504  wksfval  29678  iswlk  29679  upgr2wlk  29735  wlkiswwlks2  29943  wwlksnextfun  29966  wwlksnextinj  29967  wwlksnextbij  29970  wwlksnextprop  29980  2wlkdlem4  29996  umgr2wlk  30017  usgrwwlks2on  30026  umgrwwlks2on  30027  elwspths2spth  30038  isclwwlk  30054  clwlkclwwlklem1  30069  erclwwlkeq  30088  clwwlkn1loopb  30113  erclwwlkneq  30137  s2elclwwlknon2  30174  3wlkdlem5  30233  3wlkdlem6  30235  3wlkdlem9  30238  3wlkdlem10  30239  uhgr3cyclex  30252  upgr4cycl4dv4e  30255  frgr3v  30345  3cyclfrgrrn1  30355  extwwlkfabel  30423  isplig  30547  lpni  30551  isgrpo  30568  vciOLD  30632  isvclem  30648  isnvlem  30681  sspval  30794  isssp  30795  ajfval  30880  dipdir  30913  siilem2  30923  issh  31279  elunop2  32084  superpos  32425  padct  32791  isslmd  33263  slmdlema  33264  subsdrg  33359  elrspunidl  33488  constrcbvlem  33899  locfinreflem  33984  locfinref  33985  zarcmplem  34025  zhmnrg  34109  ismntoplly  34169  issiga  34256  isrnsiga  34257  isldsys  34300  rossros  34324  ismeas  34343  isrnmeas  34344  pmeasmono  34468  pmeasadd  34469  istrkg2d  34810  axtgupdim2ALTV  34812  afsval  34815  brafs  34816  bnj919  34910  bnj976  34920  bnj607  35058  bnj873  35066  fineqvnttrclse  35268  tz9.1regs  35278  cvmlift3lem2  35502  cvmlift3lem6  35506  cvmlift3lem7  35507  cvmlift3lem9  35509  cvmlift3  35510  mclsppslem  35765  dfon2lem1  35963  dfon2lem3  35965  dfon2lem7  35969  brofs  36187  ofscom  36189  btwnouttr  36206  brifs  36225  cgr3com  36235  brcolinear  36241  brfs  36261  prodeq12sdv  36400  cbvproddavw2  36478  unblimceq0lem  36766  knoppndvlem21  36792  rdgeqoa  37686  poimirlem4  37945  poimirlem27  37968  mblfinlem3  37980  indexa  38054  sdclem1  38064  fdc  38066  neificl  38074  heiborlem2  38133  isass  38167  ismndo2  38195  isrngo  38218  rngomndo  38256  isgrpda  38276  igenval2  38387  eleqvrels2  38997  eleqvrels3  38998  eqvreleq  39007  lshpset2N  39565  isopos  39626  oposlem  39628  cmtfvalN  39656  cvrfval  39714  3dimlem1  39904  3dim1lem5  39912  lplni2  39983  lvoli2  40027  4atlem11  40055  dalawlem15  40331  cdlemftr3  41011  tendofset  41204  tendoset  41205  istendo  41206  cdlemk28-3  41354  cdlemkid3N  41379  cdlemkid4  41380  lpolsetN  41928  islpolN  41929  lpolconN  41933  isprimroot  42532  aks6d1c1p1  42546  ismrc  43133  rabren3dioph  43243  irrapxlem5  43254  rmydioph  43442  mpaaeu  43578  mpaaval  43579  mpaalem  43580  naddwordnexlem4  43829  dfsucon  43950  minregex  43961  dfrtrcl3  44160  brco3f1o  44460  grumnud  44713  modelaxreplem1  45405  modelaxreplem2  45406  modelaxrep  45408  eliooshift  45936  stoweidlem5  46433  stoweidlem18  46446  stoweidlem28  46456  stoweidlem31  46459  stoweidlem41  46469  stoweidlem43  46471  stoweidlem44  46472  stoweidlem45  46473  stoweidlem51  46479  stoweidlem55  46483  stoweidlem59  46487  issal  46742  fundcmpsurbijinjpreimafv  47867  fundcmpsurbijinj  47870  fundcmpsurinjALT  47872  ichnreuop  47932  proththdlem  48076  6gbe  48247  8gbe  48249  bgoldbtbndlem2  48282  bgoldbtbndlem3  48283  bgoldbtbnd  48285  grtriproplem  48415  grtri  48416  grtrif1o  48418  isgrtri  48419  grimgrtri  48425  usgrexmpl1tri  48501  gpgvtx0  48529  gpgvtx1  48530  gpgedgvtx0  48537  gpgedgvtx1  48538  upwlksfval  48611  isupwlk  48612  el0ldep  48942  ldepspr  48949  lmod1  48968  zlmodzxzldep  48980  catprs  49486  catprsc  49488  prsthinc  49939  2arwcatlem1  50070  cnelsubclem  50078