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  2136  limeq  6319  f13dfv  7211  epne3  7709  oteqimp  7943  xpord2lem  8075  poxp2  8076  xpord3lem  8082  xpord3pred  8085  csbfrecsg  8217  frrlem1  8219  frrlem13  8231  smoeq  8273  on2ind  8587  on3ind  8588  naddasslem1  8612  naddasslem2  8613  naddass  8614  ereq1  8632  sbthfi  9113  indexfi  9250  hartogslem1  9434  brttrcl2  9610  ssttrcl  9611  ttrcltr  9612  ttrclss  9616  ttrclselem2  9622  tz9.1  9625  updjud  9830  alephval3  10004  cofsmo  10163  cfsmolem  10164  alephsing  10170  axdc3lem2  10345  axdc3lem3  10346  axdc3  10348  axdc4lem  10349  zornn0g  10399  fpwwe2lem4  10528  canthwelem  10544  canthwe  10545  pwfseqlem4a  10555  pwfseqlem4  10556  elwina  10580  elina  10581  iswun  10598  elgrug  10686  iccshftr  13389  iccshftl  13391  iccdil  13393  icccntr  13395  fzaddel  13461  elfzomelpfzo  13674  axdc4uzlem  13890  hash3tpb  14402  wrdl1s1  14521  wwlktovf  14863  wwlktovf1  14864  wwlktovfo  14865  wrd2f1tovbij  14867  dfrtrcl2  14969  sqrmo  15158  resqrtcl  15160  resqrtthlem  15161  sqrtneg  15174  sqreu  15268  sqrtthlem  15270  eqsqrtd  15275  prodeq1f  15813  prodeq1  15814  zprod  15844  divalglem10  16313  dfgcd2  16457  coprmprod  16572  pythagtriplem18  16744  pythagtriplem19  16745  prmgaplem3  16965  prmgaplem4  16966  isstruct2  17060  imasval  17415  mreexexlemd  17550  catidd  17586  iscatd2  17587  subsubc  17760  isfunc  17771  funcres2b  17804  ispos  18220  posi  18223  isposd  18228  pospropd  18231  resspos  18335  isps  18474  imasmnd2  18648  sgrp2rid2ex  18801  imasgrp2  18934  psgnunilem3  19375  isrngd  20058  imasrng  20062  isringd  20176  imasring  20215  subrngpropd  20453  isdrngd  20650  isdrngdOLD  20652  islmod  20767  lmodlema  20768  islmodd  20769  lmodprop2d  20827  lmhmpropd  20977  isphl  21535  isphld  21561  phlpropd  21562  mdetunilem3  22499  mdetunilem9  22505  fiinopn  22786  iscldtop  22980  lmfval  23117  connsuba  23305  1stcfb  23330  2ndcctbss  23340  subislly  23366  ptval  23455  elpt  23457  elptr  23458  upxp  23508  isfbas  23714  ustval  24088  isust  24089  ustincl  24093  ustdiag  24094  ustinvel  24095  ustexhalf  24096  ust0  24105  imasdsf1olem  24259  tngngp3  24542  lmhmclm  24985  iscph  25068  iscau2  25175  pmltpclem1  25347  isi1f  25573  mbfi1fseqlem6  25619  iblcnlem  25688  dvfsumlem4  25934  aannenlem1  26234  aannenlem2  26235  ulmval  26287  nodense  27602  nosupprefixmo  27610  noinfprefixmo  27611  nosupcbv  27612  nosupfv  27616  noinfcbv  27627  noinffv  27631  noetalem2  27652  eqscut  27716  no2indslem  27866  no3inds  27870  addsproplem3  27883  negsproplem3  27941  mulsproplem10  28033  istrkgb  28400  istrkge  28402  istrkgld  28404  istrkg2ld  28405  istrkg3ld  28406  axtgupdim2  28416  axtgeucl  28417  trgcgrg  28460  ishlg  28547  colline  28594  iscgra  28754  isinag  28783  brbtwn  28844  axpaschlem  28885  axlowdim  28906  axeuclid  28908  eengtrkge  28932  issubgr  29216  nb3grpr  29327  nb3grpr2  29328  cplgr3v  29380  wksfval  29555  iswlk  29556  upgr2wlk  29612  wlkiswwlks2  29820  wwlksnextfun  29843  wwlksnextinj  29844  wwlksnextbij  29847  wwlksnextprop  29857  2wlkdlem4  29873  umgr2wlk  29894  umgrwwlks2on  29902  elwspths2spth  29912  isclwwlk  29928  clwlkclwwlklem1  29943  erclwwlkeq  29962  clwwlkn1loopb  29987  erclwwlkneq  30011  s2elclwwlknon2  30048  3wlkdlem5  30107  3wlkdlem6  30109  3wlkdlem9  30112  3wlkdlem10  30113  uhgr3cyclex  30126  upgr4cycl4dv4e  30129  frgr3v  30219  3cyclfrgrrn1  30229  extwwlkfabel  30297  isplig  30420  lpni  30424  isgrpo  30441  vciOLD  30505  isvclem  30521  isnvlem  30554  sspval  30667  isssp  30668  ajfval  30753  dipdir  30786  siilem2  30796  issh  31152  elunop2  31957  superpos  32298  padct  32662  isslmd  33144  slmdlema  33145  subsdrg  33237  elrspunidl  33365  constrcbvlem  33722  locfinreflem  33807  locfinref  33808  zarcmplem  33848  zhmnrg  33932  ismntoplly  33992  issiga  34079  isrnsiga  34080  isldsys  34123  rossros  34147  ismeas  34166  isrnmeas  34167  pmeasmono  34292  pmeasadd  34293  istrkg2d  34634  axtgupdim2ALTV  34636  afsval  34639  brafs  34640  bnj919  34734  bnj976  34744  bnj607  34883  bnj873  34891  tz9.1regs  35067  cvmlift3lem2  35293  cvmlift3lem6  35297  cvmlift3lem7  35298  cvmlift3lem9  35300  cvmlift3  35301  mclsppslem  35556  dfon2lem1  35757  dfon2lem3  35759  dfon2lem7  35763  brofs  35979  ofscom  35981  btwnouttr  35998  brifs  36017  cgr3com  36027  brcolinear  36033  brfs  36053  prodeq12sdv  36192  cbvproddavw2  36270  unblimceq0lem  36480  knoppndvlem21  36506  rdgeqoa  37344  poimirlem4  37604  poimirlem27  37627  mblfinlem3  37639  indexa  37713  sdclem1  37723  fdc  37725  neificl  37733  heiborlem2  37792  isass  37826  ismndo2  37854  isrngo  37877  rngomndo  37915  isgrpda  37935  igenval2  38046  eleqvrels2  38569  eleqvrels3  38570  eqvreleq  38579  lshpset2N  39098  isopos  39159  oposlem  39161  cmtfvalN  39189  cvrfval  39247  3dimlem1  39437  3dim1lem5  39445  lplni2  39516  lvoli2  39560  4atlem11  39588  dalawlem15  39864  cdlemftr3  40544  tendofset  40737  tendoset  40738  istendo  40739  cdlemk28-3  40887  cdlemkid3N  40912  cdlemkid4  40913  lpolsetN  41461  islpolN  41462  lpolconN  41466  isprimroot  42066  aks6d1c1p1  42080  ismrc  42674  rabren3dioph  42788  irrapxlem5  42799  rmydioph  42987  mpaaeu  43123  mpaaval  43124  mpaalem  43125  naddwordnexlem4  43374  dfsucon  43496  minregex  43507  dfrtrcl3  43706  brco3f1o  44006  grumnud  44259  modelaxreplem1  44952  modelaxreplem2  44953  modelaxrep  44955  eliooshift  45487  stoweidlem5  45986  stoweidlem18  45999  stoweidlem28  46009  stoweidlem31  46012  stoweidlem41  46022  stoweidlem43  46024  stoweidlem44  46025  stoweidlem45  46026  stoweidlem51  46032  stoweidlem55  46036  stoweidlem59  46040  issal  46295  fundcmpsurbijinjpreimafv  47391  fundcmpsurbijinj  47394  fundcmpsurinjALT  47396  ichnreuop  47456  proththdlem  47597  6gbe  47755  8gbe  47757  bgoldbtbndlem2  47790  bgoldbtbndlem3  47791  bgoldbtbnd  47793  grtriproplem  47923  grtri  47924  grtrif1o  47926  isgrtri  47927  grimgrtri  47933  usgrexmpl1tri  48009  gpgvtx0  48037  gpgvtx1  48038  gpgedgvtx0  48045  gpgedgvtx1  48046  upwlksfval  48119  isupwlk  48120  el0ldep  48451  ldepspr  48458  lmod1  48477  zlmodzxzldep  48489  catprs  48996  catprsc  48998  prsthinc  49449  2arwcatlem1  49580  cnelsubclem  49588