Theorem 3anbi123d 1444

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

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  3anbi12d  1445  3anbi13d  1446  3anbi23d  1447  ax12wdemo  2146  limeq  6322  f13dfv  7218  epne3  7716  oteqimp  7950  xpord2lem  8082  poxp2  8083  xpord3lem  8089  xpord3pred  8092  csbfrecsg  8224  frrlem1  8226  frrlem13  8238  smoeq  8280  on2ind  8595  on3ind  8596  naddasslem1  8620  naddasslem2  8621  naddass  8622  ereq1  8641  sbthfi  9123  indexfi  9260  hartogslem1  9447  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  20540  isdrngd  20737  isdrngdOLD  20739  islmod  20854  lmodlema  20855  islmodd  20856  lmodprop2d  20914  lmhmpropd  21063  isphl  21603  isphld  21629  phlpropd  21630  mdetunilem3  22597  mdetunilem9  22603  fiinopn  22884  iscldtop  23078  lmfval  23215  connsuba  23403  1stcfb  23428  2ndcctbss  23438  subislly  23464  ptval  23553  elpt  23555  elptr  23556  upxp  23606  isfbas  23812  ustval  24186  isust  24187  ustincl  24191  ustdiag  24192  ustinvel  24193  ustexhalf  24194  ust0  24203  imasdsf1olem  24356  tngngp3  24639  lmhmclm  25072  iscph  25155  iscau2  25262  pmltpclem1  25433  isi1f  25659  mbfi1fseqlem6  25705  iblcnlem  25774  dvfsumlem4  26014  aannenlem1  26312  aannenlem2  26313  ulmval  26363  nodense  27674  nosupprefixmo  27682  noinfprefixmo  27683  nosupcbv  27684  nosupfv  27688  noinfcbv  27699  noinffv  27703  noetalem2  27724  eqcuts  27795  no2indlesm  27964  no3inds  27968  addsproplem3  27981  negsproplem3  28040  mulsproplem10  28135  bdayfinbndcbv  28476  bdayfinbndlem1  28477  bdayfinbndlem2  28478  istrkgb  28541  istrkge  28543  istrkgld  28545  istrkg2ld  28546  istrkg3ld  28547  axtgupdim2  28557  axtgeucl  28558  trgcgrg  28601  ishlg  28688  colline  28735  iscgra  28895  isinag  28924  brbtwn  28986  axpaschlem  29027  axlowdim  29048  axeuclid  29050  eengtrkge  29074  issubgr  29358  nb3grpr  29469  nb3grpr2  29470  cplgr3v  29522  wksfval  29696  iswlk  29697  upgr2wlk  29753  wlkiswwlks2  29961  wwlksnextfun  29984  wwlksnextinj  29985  wwlksnextbij  29988  wwlksnextprop  29998  2wlkdlem4  30014  umgr2wlk  30035  usgrwwlks2on  30044  umgrwwlks2on  30045  elwspths2spth  30056  isclwwlk  30072  clwlkclwwlklem1  30087  erclwwlkeq  30106  clwwlkn1loopb  30131  erclwwlkneq  30155  s2elclwwlknon2  30192  3wlkdlem5  30251  3wlkdlem6  30253  3wlkdlem9  30256  3wlkdlem10  30257  uhgr3cyclex  30270  upgr4cycl4dv4e  30273  frgr3v  30363  3cyclfrgrrn1  30373  extwwlkfabel  30441  isplig  30565  lpni  30569  isgrpo  30586  vciOLD  30650  isvclem  30666  isnvlem  30699  sspval  30812  isssp  30813  ajfval  30898  dipdir  30931  siilem2  30941  issh  31297  elunop2  32102  superpos  32443  padct  32810  isslmd  33283  slmdlema  33284  subsdrg  33382  elrspunidl  33511  constrcbvlem  33939  locfinreflem  34024  locfinref  34025  zarcmplem  34065  zhmnrg  34149  ismntoplly  34209  issiga  34296  isrnsiga  34297  isldsys  34340  rossros  34364  ismeas  34383  isrnmeas  34384  pmeasmono  34508  pmeasadd  34509  istrkg2d  34850  axtgupdim2ALTV  34852  afsval  34855  brafs  34856  bnj919  34950  bnj976  34960  bnj607  35098  bnj873  35106  fineqvnttrclse  35305  tz9.1regs  35315  cvmlift3lem2  35548  cvmlift3lem6  35552  cvmlift3lem7  35553  cvmlift3lem9  35555  cvmlift3  35556  mclsppslem  35811  dfon2lem1  36009  dfon2lem3  36011  dfon2lem7  36015  brofs  36233  ofscom  36235  btwnouttr  36252  brifs  36271  cgr3com  36281  brcolinear  36287  brfs  36307  prodeq12sdv  36446  cbvproddavw2  36524  unblimceq0lem  36812  knoppndvlem21  36838  rdgeqoa  37732  poimirlem4  37991  poimirlem27  38014  mblfinlem3  38026  indexa  38100  sdclem1  38110  fdc  38112  neificl  38120  heiborlem2  38179  isass  38213  ismndo2  38241  isrngo  38264  rngomndo  38302  isgrpda  38322  igenval2  38433  eleqvrels2  39043  eleqvrels3  39044  eqvreleq  39053  lshpset2N  39611  isopos  39672  oposlem  39674  cmtfvalN  39702  cvrfval  39760  3dimlem1  39950  3dim1lem5  39958  lplni2  40029  lvoli2  40073  4atlem11  40101  dalawlem15  40377  cdlemftr3  41057  tendofset  41250  tendoset  41251  istendo  41252  cdlemk28-3  41400  cdlemkid3N  41425  cdlemkid4  41426  lpolsetN  41974  islpolN  41975  lpolconN  41979  isprimroot  42578  aks6d1c1p1  42592  ismrc  43150  rabren3dioph  43260  irrapxlem5  43271  rmydioph  43459  mpaaeu  43595  mpaaval  43596  mpaalem  43597  naddwordnexlem4  43846  dfsucon  43967  minregex  43978  dfrtrcl3  44177  brco3f1o  44477  grumnud  44730  modelaxreplem1  45422  modelaxreplem2  45423  modelaxrep  45425  eliooshift  45951  stoweidlem5  46448  stoweidlem18  46461  stoweidlem28  46471  stoweidlem31  46474  stoweidlem41  46484  stoweidlem43  46486  stoweidlem44  46487  stoweidlem45  46488  stoweidlem51  46494  stoweidlem55  46498  stoweidlem59  46502  issal  46757  fundcmpsurbijinjpreimafv  47882  fundcmpsurbijinj  47885  fundcmpsurinjALT  47887  ichnreuop  47947  proththdlem  48091  6gbe  48262  8gbe  48264  bgoldbtbndlem2  48297  bgoldbtbndlem3  48298  bgoldbtbnd  48300  grtriproplem  48430  grtri  48431  grtrif1o  48433  isgrtri  48434  grimgrtri  48440  usgrexmpl1tri  48516  gpgvtx0  48544  gpgvtx1  48545  gpgedgvtx0  48552  gpgedgvtx1  48553  upwlksfval  48626  isupwlk  48627  el0ldep  48957  ldepspr  48964  lmod1  48983  zlmodzxzldep  48995  catprs  49501  catprsc  49503  prsthinc  49954  2arwcatlem1  50085  cnelsubclem  50093