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  6326  f13dfv  7217  epne3  7715  oteqimp  7949  xpord2lem  8081  poxp2  8082  xpord3lem  8088  xpord3pred  8091  csbfrecsg  8223  frrlem1  8225  frrlem13  8237  smoeq  8279  on2ind  8593  on3ind  8594  naddasslem1  8618  naddasslem2  8619  naddass  8620  ereq1  8638  sbthfi  9119  indexfi  9255  hartogslem1  9439  brttrcl2  9615  ssttrcl  9616  ttrcltr  9617  ttrclss  9621  ttrclselem2  9627  tz9.1  9630  updjud  9838  alephval3  10012  cofsmo  10171  cfsmolem  10172  alephsing  10178  axdc3lem2  10353  axdc3lem3  10354  axdc3  10356  axdc4lem  10357  zornn0g  10407  fpwwe2lem4  10536  canthwelem  10552  canthwe  10553  pwfseqlem4a  10563  pwfseqlem4  10564  elwina  10588  elina  10589  iswun  10606  elgrug  10694  iccshftr  13393  iccshftl  13395  iccdil  13397  icccntr  13399  fzaddel  13465  elfzomelpfzo  13679  axdc4uzlem  13897  hash3tpb  14409  wrdl1s1  14529  wwlktovf  14870  wwlktovf1  14871  wwlktovfo  14872  wrd2f1tovbij  14874  dfrtrcl2  14976  sqrmo  15165  resqrtcl  15167  resqrtthlem  15168  sqrtneg  15181  sqreu  15275  sqrtthlem  15277  eqsqrtd  15282  prodeq1f  15820  prodeq1  15821  zprod  15851  divalglem10  16320  dfgcd2  16464  coprmprod  16579  pythagtriplem18  16751  pythagtriplem19  16752  prmgaplem3  16972  prmgaplem4  16973  isstruct2  17067  imasval  17423  mreexexlemd  17558  catidd  17594  iscatd2  17595  subsubc  17768  isfunc  17779  funcres2b  17812  ispos  18228  posi  18231  isposd  18236  pospropd  18239  resspos  18343  isps  18482  imasmnd2  18690  sgrp2rid2ex  18843  imasgrp2  18976  psgnunilem3  19416  isrngd  20099  imasrng  20103  isringd  20217  imasring  20257  subrngpropd  20492  isdrngd  20689  isdrngdOLD  20691  islmod  20806  lmodlema  20807  islmodd  20808  lmodprop2d  20866  lmhmpropd  21016  isphl  21574  isphld  21600  phlpropd  21601  mdetunilem3  22549  mdetunilem9  22555  fiinopn  22836  iscldtop  23030  lmfval  23167  connsuba  23355  1stcfb  23380  2ndcctbss  23390  subislly  23416  ptval  23505  elpt  23507  elptr  23508  upxp  23558  isfbas  23764  ustval  24138  isust  24139  ustincl  24143  ustdiag  24144  ustinvel  24145  ustexhalf  24146  ust0  24155  imasdsf1olem  24308  tngngp3  24591  lmhmclm  25034  iscph  25117  iscau2  25224  pmltpclem1  25396  isi1f  25622  mbfi1fseqlem6  25668  iblcnlem  25737  dvfsumlem4  25983  aannenlem1  26283  aannenlem2  26284  ulmval  26336  nodense  27651  nosupprefixmo  27659  noinfprefixmo  27660  nosupcbv  27661  nosupfv  27665  noinfcbv  27676  noinffv  27680  noetalem2  27701  eqscut  27766  no2indslem  27917  no3inds  27921  addsproplem3  27934  negsproplem3  27992  mulsproplem10  28084  istrkgb  28453  istrkge  28455  istrkgld  28457  istrkg2ld  28458  istrkg3ld  28459  axtgupdim2  28469  axtgeucl  28470  trgcgrg  28513  ishlg  28600  colline  28647  iscgra  28807  isinag  28836  brbtwn  28898  axpaschlem  28939  axlowdim  28960  axeuclid  28962  eengtrkge  28986  issubgr  29270  nb3grpr  29381  nb3grpr2  29382  cplgr3v  29434  wksfval  29609  iswlk  29610  upgr2wlk  29666  wlkiswwlks2  29874  wwlksnextfun  29897  wwlksnextinj  29898  wwlksnextbij  29901  wwlksnextprop  29911  2wlkdlem4  29927  umgr2wlk  29948  usgrwwlks2on  29957  umgrwwlks2on  29958  elwspths2spth  29969  isclwwlk  29985  clwlkclwwlklem1  30000  erclwwlkeq  30019  clwwlkn1loopb  30044  erclwwlkneq  30068  s2elclwwlknon2  30105  3wlkdlem5  30164  3wlkdlem6  30166  3wlkdlem9  30169  3wlkdlem10  30170  uhgr3cyclex  30183  upgr4cycl4dv4e  30186  frgr3v  30276  3cyclfrgrrn1  30286  extwwlkfabel  30354  isplig  30477  lpni  30481  isgrpo  30498  vciOLD  30562  isvclem  30578  isnvlem  30611  sspval  30724  isssp  30725  ajfval  30810  dipdir  30843  siilem2  30853  issh  31209  elunop2  32014  superpos  32355  padct  32725  isslmd  33212  slmdlema  33213  subsdrg  33308  elrspunidl  33437  constrcbvlem  33840  locfinreflem  33925  locfinref  33926  zarcmplem  33966  zhmnrg  34050  ismntoplly  34110  issiga  34197  isrnsiga  34198  isldsys  34241  rossros  34265  ismeas  34284  isrnmeas  34285  pmeasmono  34409  pmeasadd  34410  istrkg2d  34751  axtgupdim2ALTV  34753  afsval  34756  brafs  34757  bnj919  34851  bnj976  34861  bnj607  35000  bnj873  35008  tz9.1regs  35202  fineqvnttrclse  35216  cvmlift3lem2  35436  cvmlift3lem6  35440  cvmlift3lem7  35441  cvmlift3lem9  35443  cvmlift3  35444  mclsppslem  35699  dfon2lem1  35897  dfon2lem3  35899  dfon2lem7  35903  brofs  36121  ofscom  36123  btwnouttr  36140  brifs  36159  cgr3com  36169  brcolinear  36175  brfs  36195  prodeq12sdv  36334  cbvproddavw2  36412  unblimceq0lem  36622  knoppndvlem21  36648  rdgeqoa  37487  poimirlem4  37737  poimirlem27  37760  mblfinlem3  37772  indexa  37846  sdclem1  37856  fdc  37858  neificl  37866  heiborlem2  37925  isass  37959  ismndo2  37987  isrngo  38010  rngomndo  38048  isgrpda  38068  igenval2  38179  eleqvrels2  38761  eleqvrels3  38762  eqvreleq  38771  lshpset2N  39291  isopos  39352  oposlem  39354  cmtfvalN  39382  cvrfval  39440  3dimlem1  39630  3dim1lem5  39638  lplni2  39709  lvoli2  39753  4atlem11  39781  dalawlem15  40057  cdlemftr3  40737  tendofset  40930  tendoset  40931  istendo  40932  cdlemk28-3  41080  cdlemkid3N  41105  cdlemkid4  41106  lpolsetN  41654  islpolN  41655  lpolconN  41659  isprimroot  42259  aks6d1c1p1  42273  ismrc  42858  rabren3dioph  42972  irrapxlem5  42983  rmydioph  43171  mpaaeu  43307  mpaaval  43308  mpaalem  43309  naddwordnexlem4  43558  dfsucon  43680  minregex  43691  dfrtrcl3  43890  brco3f1o  44190  grumnud  44443  modelaxreplem1  45135  modelaxreplem2  45136  modelaxrep  45138  eliooshift  45668  stoweidlem5  46165  stoweidlem18  46178  stoweidlem28  46188  stoweidlem31  46191  stoweidlem41  46201  stoweidlem43  46203  stoweidlem44  46204  stoweidlem45  46205  stoweidlem51  46211  stoweidlem55  46215  stoweidlem59  46219  issal  46474  fundcmpsurbijinjpreimafv  47569  fundcmpsurbijinj  47572  fundcmpsurinjALT  47574  ichnreuop  47634  proththdlem  47775  6gbe  47933  8gbe  47935  bgoldbtbndlem2  47968  bgoldbtbndlem3  47969  bgoldbtbnd  47971  grtriproplem  48101  grtri  48102  grtrif1o  48104  isgrtri  48105  grimgrtri  48111  usgrexmpl1tri  48187  gpgvtx0  48215  gpgvtx1  48216  gpgedgvtx0  48223  gpgedgvtx1  48224  upwlksfval  48297  isupwlk  48298  el0ldep  48628  ldepspr  48635  lmod1  48654  zlmodzxzldep  48666  catprs  49172  catprsc  49174  prsthinc  49625  2arwcatlem1  49756  cnelsubclem  49764