Theorem 3anbi123d 1438

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  3anbi12d  1439  3anbi13d  1440  3anbi23d  1441  ax12wdemo  2140  limeq  6329  f13dfv  7220  epne3  7718  oteqimp  7952  xpord2lem  8084  poxp2  8085  xpord3lem  8091  xpord3pred  8094  csbfrecsg  8226  frrlem1  8228  frrlem13  8240  smoeq  8282  on2ind  8597  on3ind  8598  naddasslem1  8622  naddasslem2  8623  naddass  8624  ereq1  8642  sbthfi  9123  indexfi  9260  hartogslem1  9447  brttrcl2  9623  ssttrcl  9624  ttrcltr  9625  ttrclss  9629  ttrclselem2  9635  tz9.1  9638  updjud  9846  alephval3  10020  cofsmo  10179  cfsmolem  10180  alephsing  10186  axdc3lem2  10361  axdc3lem3  10362  axdc3  10364  axdc4lem  10365  zornn0g  10415  fpwwe2lem4  10545  canthwelem  10561  canthwe  10562  pwfseqlem4a  10572  pwfseqlem4  10573  elwina  10597  elina  10598  iswun  10615  elgrug  10703  iccshftr  13402  iccshftl  13404  iccdil  13406  icccntr  13408  fzaddel  13474  elfzomelpfzo  13688  axdc4uzlem  13906  hash3tpb  14418  wrdl1s1  14538  wwlktovf  14879  wwlktovf1  14880  wwlktovfo  14881  wrd2f1tovbij  14883  dfrtrcl2  14985  sqrmo  15174  resqrtcl  15176  resqrtthlem  15177  sqrtneg  15190  sqreu  15284  sqrtthlem  15286  eqsqrtd  15291  prodeq1f  15829  prodeq1  15830  zprod  15860  divalglem10  16329  dfgcd2  16473  coprmprod  16588  pythagtriplem18  16760  pythagtriplem19  16761  prmgaplem3  16981  prmgaplem4  16982  isstruct2  17076  imasval  17432  mreexexlemd  17567  catidd  17603  iscatd2  17604  subsubc  17777  isfunc  17788  funcres2b  17821  ispos  18237  posi  18240  isposd  18245  pospropd  18248  resspos  18352  isps  18491  imasmnd2  18699  sgrp2rid2ex  18852  imasgrp2  18985  psgnunilem3  19425  isrngd  20108  imasrng  20112  isringd  20226  imasring  20266  subrngpropd  20501  isdrngd  20698  isdrngdOLD  20700  islmod  20815  lmodlema  20816  islmodd  20817  lmodprop2d  20875  lmhmpropd  21025  isphl  21583  isphld  21609  phlpropd  21610  mdetunilem3  22558  mdetunilem9  22564  fiinopn  22845  iscldtop  23039  lmfval  23176  connsuba  23364  1stcfb  23389  2ndcctbss  23399  subislly  23425  ptval  23514  elpt  23516  elptr  23517  upxp  23567  isfbas  23773  ustval  24147  isust  24148  ustincl  24152  ustdiag  24153  ustinvel  24154  ustexhalf  24155  ust0  24164  imasdsf1olem  24317  tngngp3  24600  lmhmclm  25043  iscph  25126  iscau2  25233  pmltpclem1  25405  isi1f  25631  mbfi1fseqlem6  25677  iblcnlem  25746  dvfsumlem4  25992  aannenlem1  26292  aannenlem2  26293  ulmval  26345  nodense  27660  nosupprefixmo  27668  noinfprefixmo  27669  nosupcbv  27670  nosupfv  27674  noinfcbv  27685  noinffv  27689  noetalem2  27710  eqcuts  27781  no2indlesm  27950  no3inds  27954  addsproplem3  27967  negsproplem3  28026  mulsproplem10  28121  bdayfinbndcbv  28462  bdayfinbndlem1  28463  bdayfinbndlem2  28464  istrkgb  28527  istrkge  28529  istrkgld  28531  istrkg2ld  28532  istrkg3ld  28533  axtgupdim2  28543  axtgeucl  28544  trgcgrg  28587  ishlg  28674  colline  28721  iscgra  28881  isinag  28910  brbtwn  28972  axpaschlem  29013  axlowdim  29034  axeuclid  29036  eengtrkge  29060  issubgr  29344  nb3grpr  29455  nb3grpr2  29456  cplgr3v  29508  wksfval  29683  iswlk  29684  upgr2wlk  29740  wlkiswwlks2  29948  wwlksnextfun  29971  wwlksnextinj  29972  wwlksnextbij  29975  wwlksnextprop  29985  2wlkdlem4  30001  umgr2wlk  30022  usgrwwlks2on  30031  umgrwwlks2on  30032  elwspths2spth  30043  isclwwlk  30059  clwlkclwwlklem1  30074  erclwwlkeq  30093  clwwlkn1loopb  30118  erclwwlkneq  30142  s2elclwwlknon2  30179  3wlkdlem5  30238  3wlkdlem6  30240  3wlkdlem9  30243  3wlkdlem10  30244  uhgr3cyclex  30257  upgr4cycl4dv4e  30260  frgr3v  30350  3cyclfrgrrn1  30360  extwwlkfabel  30428  isplig  30551  lpni  30555  isgrpo  30572  vciOLD  30636  isvclem  30652  isnvlem  30685  sspval  30798  isssp  30799  ajfval  30884  dipdir  30917  siilem2  30927  issh  31283  elunop2  32088  superpos  32429  padct  32797  isslmd  33284  slmdlema  33285  subsdrg  33380  elrspunidl  33509  constrcbvlem  33912  locfinreflem  33997  locfinref  33998  zarcmplem  34038  zhmnrg  34122  ismntoplly  34182  issiga  34269  isrnsiga  34270  isldsys  34313  rossros  34337  ismeas  34356  isrnmeas  34357  pmeasmono  34481  pmeasadd  34482  istrkg2d  34823  axtgupdim2ALTV  34825  afsval  34828  brafs  34829  bnj919  34923  bnj976  34933  bnj607  35072  bnj873  35080  fineqvnttrclse  35280  tz9.1regs  35290  cvmlift3lem2  35514  cvmlift3lem6  35518  cvmlift3lem7  35519  cvmlift3lem9  35521  cvmlift3  35522  mclsppslem  35777  dfon2lem1  35975  dfon2lem3  35977  dfon2lem7  35981  brofs  36199  ofscom  36201  btwnouttr  36218  brifs  36237  cgr3com  36247  brcolinear  36253  brfs  36273  prodeq12sdv  36412  cbvproddavw2  36490  unblimceq0lem  36706  knoppndvlem21  36732  rdgeqoa  37575  poimirlem4  37825  poimirlem27  37848  mblfinlem3  37860  indexa  37934  sdclem1  37944  fdc  37946  neificl  37954  heiborlem2  38013  isass  38047  ismndo2  38075  isrngo  38098  rngomndo  38136  isgrpda  38156  igenval2  38267  eleqvrels2  38849  eleqvrels3  38850  eqvreleq  38859  lshpset2N  39379  isopos  39440  oposlem  39442  cmtfvalN  39470  cvrfval  39528  3dimlem1  39718  3dim1lem5  39726  lplni2  39797  lvoli2  39841  4atlem11  39869  dalawlem15  40145  cdlemftr3  40825  tendofset  41018  tendoset  41019  istendo  41020  cdlemk28-3  41168  cdlemkid3N  41193  cdlemkid4  41194  lpolsetN  41742  islpolN  41743  lpolconN  41747  isprimroot  42347  aks6d1c1p1  42361  ismrc  42943  rabren3dioph  43057  irrapxlem5  43068  rmydioph  43256  mpaaeu  43392  mpaaval  43393  mpaalem  43394  naddwordnexlem4  43643  dfsucon  43764  minregex  43775  dfrtrcl3  43974  brco3f1o  44274  grumnud  44527  modelaxreplem1  45219  modelaxreplem2  45220  modelaxrep  45222  eliooshift  45752  stoweidlem5  46249  stoweidlem18  46262  stoweidlem28  46272  stoweidlem31  46275  stoweidlem41  46285  stoweidlem43  46287  stoweidlem44  46288  stoweidlem45  46289  stoweidlem51  46295  stoweidlem55  46299  stoweidlem59  46303  issal  46558  fundcmpsurbijinjpreimafv  47653  fundcmpsurbijinj  47656  fundcmpsurinjALT  47658  ichnreuop  47718  proththdlem  47859  6gbe  48017  8gbe  48019  bgoldbtbndlem2  48052  bgoldbtbndlem3  48053  bgoldbtbnd  48055  grtriproplem  48185  grtri  48186  grtrif1o  48188  isgrtri  48189  grimgrtri  48195  usgrexmpl1tri  48271  gpgvtx0  48299  gpgvtx1  48300  gpgedgvtx0  48307  gpgedgvtx1  48308  upwlksfval  48381  isupwlk  48382  el0ldep  48712  ldepspr  48719  lmod1  48738  zlmodzxzldep  48750  catprs  49256  catprsc  49258  prsthinc  49709  2arwcatlem1  49840  cnelsubclem  49848