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  2171  limeq  6376  f13dfv  7284  epne3  7789  oteqimp  8022  xpord2lem  8163  poxp2  8164  xpord3lem  8170  xpord3pred  8173  csbfrecsg  8307  frrlem1  8309  frrlem13  8321  smoeq  8363  on2ind  8683  on3ind  8684  naddasslem1  8709  naddasslem2  8710  naddass  8711  ereq1  8730  sbthfi  9219  indexfi  9354  hartogslem1  9541  brttrcl2  9720  ssttrcl  9721  ttrcltr  9722  ttrclss  9726  ttrclselem2  9732  tz9.1  9735  updjud  10020  alephval3  10194  cofsmo  10352  cfsmolem  10353  alephsing  10359  axdc3lem2  10534  axdc3lem3  10535  axdc3  10537  axdc4lem  10538  zornn0g  10588  fpwwe2lem4  10724  canthwelem  10740  canthwe  10741  pwfseqlem4a  10751  pwfseqlem4  10752  elwina  10776  elina  10777  iswun  10794  elgrug  10882  iccshftr  13622  iccshftl  13624  iccdil  13626  icccntr  13628  fzaddel  13697  elfzomelpfzo  13912  axdc4uzlem  14131  hash3tpb  14645  wrdl1s1  14768  wwlktovf  15116  wwlktovf1  15117  wwlktovfo  15118  wrd2f1tovbij  15120  dfrtrcl2  15222  sqrmo  15425  resqrtcl  15427  resqrtthlem  15428  sqrtneg  15441  sqreu  15535  sqrtthlem  15537  eqsqrtd  15542  prodeq1f  16082  prodeq1  16083  zprod  16111  divalglem10  16579  dfgcd2  16726  coprmprod  16843  pythagtriplem18  17017  pythagtriplem19  17018  prmgaplem3  17238  prmgaplem4  17239  isstruct2  17334  imasval  17690  mreexexlemd  17825  catidd  17861  iscatd2  17862  subsubc  18035  isfunc  18046  funcres2b  18079  ispos  18495  posi  18498  isposd  18503  pospropd  18506  resspos  18610  isps  18749  imasmnd2  18975  sgrp2rid2ex  19133  imasgrp2  19272  psgnunilem3  19717  isrngd  20402  imasrng  20406  isringd  20529  imasring  20567  subrngpropd  20827  isdrngd  21029  isdrngdOLD  21031  islmod  21146  lmodlema  21147  islmodd  21148  lmodprop2d  21206  lmhmpropd  21355  rspprop  21531  isphl  21941  isphld  21967  phlpropd  21968  mdetunilem3  22936  mdetunilem9  22942  fiinopn  23226  iscldtop  23420  lmfval  23557  connsuba  23745  1stcfb  23770  2ndcctbss  23781  subislly  23807  ptval  23896  elpt  23898  elptr  23899  upxp  23949  isfbas  24155  ustval  24529  isust  24530  ustincl  24534  ustdiag  24535  ustinvel  24536  ustexhalf  24537  ust0  24546  imasdsf1olem  24699  tngngp3  24982  lmhmclm  25415  iscph  25498  iscau2  25605  pmltpclem1  25776  isi1f  26002  mbfi1fseqlem6  26048  iblcnlem  26116  dvfsumlem4  26356  aannenlem1  26662  aannenlem2  26663  ulmval  26714  nodense  28056  nosupprefixmo  28064  noinfprefixmo  28065  nosupcbv  28066  nosupfv  28070  noinfcbv  28081  noinffv  28085  noetalem2  28106  eqcuts  28178  no2indlesm  28347  no3inds  28351  addsproplem3  28364  negsproplem3  28423  mulsproplem10  28518  bdayfinbndcbv  28859  bdayfinbndlem1  28860  bdayfinbndlem2  28861  istrkgb  28924  istrkge  28926  istrkgld  28928  istrkg2ld  28929  istrkg3ld  28930  axtgupdim2  28940  axtgeucl  28941  trgcgrg  28985  ishlg2  29072  ishlg  29075  colline  29125  iscgra  29323  isinag  29364  cgrabasimass  29385  angmgmaddov1  29395  angmgmaddcl  29398  angmgmval  29401  brbtwn  29484  axpaschlem  29525  axlowdim  29546  axeuclid  29548  eengtrkge  29572  issubgr  29859  nb3grpr  29970  nb3grpr2  29971  cplgr3v  30023  wksfval  30197  iswlk  30198  upgr2wlk  30254  wlkiswwlks2  30471  wwlksnextfun  30494  wwlksnextinj  30495  wwlksnextbij  30498  wwlksnextprop  30508  2wlkdlem4  30524  umgr2wlk  30545  usgrwwlks2on  30554  umgrwwlks2on  30555  elwspths2spth  30566  isclwwlk  30582  clwlkclwwlklem1  30597  erclwwlkeq  30616  clwwlkn1loopb  30641  erclwwlkneq  30665  s2elclwwlknon2  30702  3wlkdlem5  30771  3wlkdlem6  30773  3wlkdlem9  30776  3wlkdlem10  30777  uhgr3cyclex  30790  upgr4cycl4dv4e  30793  frgr3v  30883  3cyclfrgrrn1  30893  extwwlkfabel  30961  isplig  31085  lpni  31089  isgrpo  31106  vciOLD  31170  isvclem  31186  isnvlem  31219  sspval  31332  isssp  31333  ajfval  31418  dipdir  31451  siilem2  31461  issh  31817  elunop2  32622  superpos  32963  padct  33359  isslmd  33811  slmdlema  33812  subsdrg  33908  elrspunidl  34026  constrcbvlem  34435  locfinreflem  34520  locfinref  34521  zarcmplem  34561  zhmnrg  34645  ismntoplly  34705  issiga  34792  isrnsiga  34793  isldsys  34837  rossros  34861  ismeas  34880  isrnmeas  34881  pmeasmono  35004  pmeasadd  35005  istrkg2d  35343  axtgupdim2ALTV  35345  afsval  35351  brafs  35352  bnj919  35446  bnj976  35456  bnj607  35594  bnj873  35602  weexenwe  35814  fineqvnttrclse  35850  tz9.1regs  35860  onprcf1acwevdlem1  35966  srepdflem2  36007  srepdf  36008  cvmlift3lem2  36173  cvmlift3lem6  36177  cvmlift3lem7  36178  cvmlift3lem9  36180  cvmlift3  36181  mclsppslem  36436  mirimanoffr  36548  dfon2lem3  36641  dfon2lem7  36645  brofs  36864  ofscom  36866  btwnouttr  36883  brifs  36902  cgr3com  36912  brcolinear  36918  brfs  36938  prodeq12sdv  37101  cbvproddavw2  37179  unblimceq0lem  37466  knoppndvlem21  37492  rdgeqoa  38400  poimirlem4  38649  poimirlem27  38672  mblfinlem3  38684  indexa  38774  sdclem1  38784  fdc  38786  neificl  38794  heiborlem2  38853  isass  38887  ismndo2  38915  isrngo  38938  rngomndo  38976  isgrpda  38996  igenval2  39107  eleqvrels2  39715  eleqvrels3  39716  eqvreleq  39725  lshpset2N  40283  isopos  40344  oposlem  40346  cmtfvalN  40374  cvrfval  40432  3dimlem1  40622  3dim1lem5  40630  lplni2  40701  lvoli2  40745  4atlem11  40773  dalawlem15  41049  cdlemftr3  41729  tendofset  41922  tendoset  41923  istendo  41924  cdlemk28-3  42072  cdlemkid3N  42097  cdlemkid4  42098  lpolsetN  42646  islpolN  42647  lpolconN  42651  isprimroot  43250  aks6d1c1p1  43264  ismrc  43819  rabren3dioph  43929  irrapxlem5  43940  rmydioph  44128  mpaaeu  44259  mpaaval  44260  mpaalem  44261  naddwordnexlem4  44510  dfsucon  44631  minregex  44642  dfrtrcl3  44840  brco3f1o  45140  grumnud  45377  modelaxreplem1  46075  modelaxreplem2  46076  modelaxrep  46078  eliooshift  46625  stoweidlem5  47122  stoweidlem18  47135  stoweidlem28  47145  stoweidlem31  47148  stoweidlem41  47158  stoweidlem43  47160  stoweidlem44  47161  stoweidlem45  47162  stoweidlem51  47168  stoweidlem55  47172  stoweidlem59  47176  issal  47431  fundcmpsurbijinjpreimafv  48596  fundcmpsurbijinj  48599  fundcmpsurinjALT  48601  ichnreuop  48661  proththdlem  48805  6gbe  48976  8gbe  48978  bgoldbtbndlem2  49011  bgoldbtbndlem3  49012  bgoldbtbnd  49014  grtriproplem  49144  grtri  49145  grtrif1o  49147  isgrtri  49148  grimgrtri  49154  usgrexmpl1tri  49230  gpgvtx0  49258  gpgvtx1  49259  gpgedgvtx0  49266  gpgedgvtx1  49267  upwlksfval  49340  isupwlk  49341  el0ldep  49685  ldepspr  49692  lmod1  49711  zlmodzxzldep  49723  catprs  50232  catprsc  50234  prsthinc  50706  2arwcatlem1  50840  cnelsubcw  50848