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  6337  f13dfv  7230  epne3  7728  oteqimp  7962  xpord2lem  8094  poxp2  8095  xpord3lem  8101  xpord3pred  8104  csbfrecsg  8236  frrlem1  8238  frrlem13  8250  smoeq  8292  on2ind  8607  on3ind  8608  naddasslem1  8632  naddasslem2  8633  naddass  8634  ereq1  8653  sbthfi  9135  indexfi  9272  hartogslem1  9459  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  13414  iccshftl  13416  iccdil  13418  icccntr  13420  fzaddel  13486  elfzomelpfzo  13700  axdc4uzlem  13918  hash3tpb  14430  wrdl1s1  14550  wwlktovf  14891  wwlktovf1  14892  wwlktovfo  14893  wrd2f1tovbij  14895  dfrtrcl2  14997  sqrmo  15186  resqrtcl  15188  resqrtthlem  15189  sqrtneg  15202  sqreu  15296  sqrtthlem  15298  eqsqrtd  15303  prodeq1f  15841  prodeq1  15842  zprod  15872  divalglem10  16341  dfgcd2  16485  coprmprod  16600  pythagtriplem18  16772  pythagtriplem19  16773  prmgaplem3  16993  prmgaplem4  16994  isstruct2  17088  imasval  17444  mreexexlemd  17579  catidd  17615  iscatd2  17616  subsubc  17789  isfunc  17800  funcres2b  17833  ispos  18249  posi  18252  isposd  18257  pospropd  18260  resspos  18364  isps  18503  imasmnd2  18711  sgrp2rid2ex  18864  imasgrp2  18997  psgnunilem3  19437  isrngd  20120  imasrng  20124  isringd  20238  imasring  20278  subrngpropd  20513  isdrngd  20710  isdrngdOLD  20712  islmod  20827  lmodlema  20828  islmodd  20829  lmodprop2d  20887  lmhmpropd  21037  isphl  21595  isphld  21621  phlpropd  21622  mdetunilem3  22570  mdetunilem9  22576  fiinopn  22857  iscldtop  23051  lmfval  23188  connsuba  23376  1stcfb  23401  2ndcctbss  23411  subislly  23437  ptval  23526  elpt  23528  elptr  23529  upxp  23579  isfbas  23785  ustval  24159  isust  24160  ustincl  24164  ustdiag  24165  ustinvel  24166  ustexhalf  24167  ust0  24176  imasdsf1olem  24329  tngngp3  24612  lmhmclm  25055  iscph  25138  iscau2  25245  pmltpclem1  25417  isi1f  25643  mbfi1fseqlem6  25689  iblcnlem  25758  dvfsumlem4  26004  aannenlem1  26304  aannenlem2  26305  ulmval  26357  nodense  27672  nosupprefixmo  27680  noinfprefixmo  27681  nosupcbv  27682  nosupfv  27686  noinfcbv  27697  noinffv  27701  noetalem2  27722  eqcuts  27793  no2indlesm  27962  no3inds  27966  addsproplem3  27979  negsproplem3  28038  mulsproplem10  28133  bdayfinbndcbv  28474  bdayfinbndlem1  28475  bdayfinbndlem2  28476  istrkgb  28539  istrkge  28541  istrkgld  28543  istrkg2ld  28544  istrkg3ld  28545  axtgupdim2  28555  axtgeucl  28556  trgcgrg  28599  ishlg  28686  colline  28733  iscgra  28893  isinag  28922  brbtwn  28984  axpaschlem  29025  axlowdim  29046  axeuclid  29048  eengtrkge  29072  issubgr  29356  nb3grpr  29467  nb3grpr2  29468  cplgr3v  29520  wksfval  29695  iswlk  29696  upgr2wlk  29752  wlkiswwlks2  29960  wwlksnextfun  29983  wwlksnextinj  29984  wwlksnextbij  29987  wwlksnextprop  29997  2wlkdlem4  30013  umgr2wlk  30034  usgrwwlks2on  30043  umgrwwlks2on  30044  elwspths2spth  30055  isclwwlk  30071  clwlkclwwlklem1  30086  erclwwlkeq  30105  clwwlkn1loopb  30130  erclwwlkneq  30154  s2elclwwlknon2  30191  3wlkdlem5  30250  3wlkdlem6  30252  3wlkdlem9  30255  3wlkdlem10  30256  uhgr3cyclex  30269  upgr4cycl4dv4e  30272  frgr3v  30362  3cyclfrgrrn1  30372  extwwlkfabel  30440  isplig  30564  lpni  30568  isgrpo  30585  vciOLD  30649  isvclem  30665  isnvlem  30698  sspval  30811  isssp  30812  ajfval  30897  dipdir  30930  siilem2  30940  issh  31296  elunop2  32101  superpos  32442  padct  32808  isslmd  33296  slmdlema  33297  subsdrg  33392  elrspunidl  33521  constrcbvlem  33933  locfinreflem  34018  locfinref  34019  zarcmplem  34059  zhmnrg  34143  ismntoplly  34203  issiga  34290  isrnsiga  34291  isldsys  34334  rossros  34358  ismeas  34377  isrnmeas  34378  pmeasmono  34502  pmeasadd  34503  istrkg2d  34844  axtgupdim2ALTV  34846  afsval  34849  brafs  34850  bnj919  34944  bnj976  34954  bnj607  35092  bnj873  35100  fineqvnttrclse  35302  tz9.1regs  35312  cvmlift3lem2  35536  cvmlift3lem6  35540  cvmlift3lem7  35541  cvmlift3lem9  35543  cvmlift3  35544  mclsppslem  35799  dfon2lem1  35997  dfon2lem3  35999  dfon2lem7  36003  brofs  36221  ofscom  36223  btwnouttr  36240  brifs  36259  cgr3com  36269  brcolinear  36275  brfs  36295  prodeq12sdv  36434  cbvproddavw2  36512  unblimceq0lem  36728  knoppndvlem21  36754  rdgeqoa  37625  poimirlem4  37875  poimirlem27  37898  mblfinlem3  37910  indexa  37984  sdclem1  37994  fdc  37996  neificl  38004  heiborlem2  38063  isass  38097  ismndo2  38125  isrngo  38148  rngomndo  38186  isgrpda  38206  igenval2  38317  eleqvrels2  38927  eleqvrels3  38928  eqvreleq  38937  lshpset2N  39495  isopos  39556  oposlem  39558  cmtfvalN  39586  cvrfval  39644  3dimlem1  39834  3dim1lem5  39842  lplni2  39913  lvoli2  39957  4atlem11  39985  dalawlem15  40261  cdlemftr3  40941  tendofset  41134  tendoset  41135  istendo  41136  cdlemk28-3  41284  cdlemkid3N  41309  cdlemkid4  41310  lpolsetN  41858  islpolN  41859  lpolconN  41863  isprimroot  42463  aks6d1c1p1  42477  ismrc  43058  rabren3dioph  43172  irrapxlem5  43183  rmydioph  43371  mpaaeu  43507  mpaaval  43508  mpaalem  43509  naddwordnexlem4  43758  dfsucon  43879  minregex  43890  dfrtrcl3  44089  brco3f1o  44389  grumnud  44642  modelaxreplem1  45334  modelaxreplem2  45335  modelaxrep  45337  eliooshift  45866  stoweidlem5  46363  stoweidlem18  46376  stoweidlem28  46386  stoweidlem31  46389  stoweidlem41  46399  stoweidlem43  46401  stoweidlem44  46402  stoweidlem45  46403  stoweidlem51  46409  stoweidlem55  46413  stoweidlem59  46417  issal  46672  fundcmpsurbijinjpreimafv  47767  fundcmpsurbijinj  47770  fundcmpsurinjALT  47772  ichnreuop  47832  proththdlem  47973  6gbe  48131  8gbe  48133  bgoldbtbndlem2  48166  bgoldbtbndlem3  48167  bgoldbtbnd  48169  grtriproplem  48299  grtri  48300  grtrif1o  48302  isgrtri  48303  grimgrtri  48309  usgrexmpl1tri  48385  gpgvtx0  48413  gpgvtx1  48414  gpgedgvtx0  48421  gpgedgvtx1  48422  upwlksfval  48495  isupwlk  48496  el0ldep  48826  ldepspr  48833  lmod1  48852  zlmodzxzldep  48864  catprs  49370  catprsc  49372  prsthinc  49823  2arwcatlem1  49954  cnelsubclem  49962