MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3anbi123d Unicode version

Theorem 3anbi123d 1299
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
StepHypRef Expression
1 bi3d.1 . . . 4
2 bi3d.2 . . . 4
31, 2anbi12d 710 . . 3
4 bi3d.3 . . 3
53, 4anbi12d 710 . 2
6 df-3an 975 . 2
7 df-3an 975 . 2
85, 6, 73bitr4g 288 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  /\w3a 973
This theorem is referenced by:  3anbi12d  1300  3anbi13d  1301  3anbi23d  1302  ax12wdemo  1831  sbc3angOLD  3391  limeq  4895  f13dfv  6180  epne3  6616  oteqimp  6819  smoeq  7040  ereq1  7337  indexfi  7848  hartogslem1  7988  tz9.1  8181  alephval3  8512  cofsmo  8670  cfsmolem  8671  alephsing  8677  axdc3lem2  8852  axdc3lem3  8853  axdc3  8855  axdc4lem  8856  zornn0g  8906  fpwwe2lem5  9033  canthwelem  9049  canthwe  9050  pwfseqlem4a  9060  pwfseqlem4  9061  elwina  9085  elina  9086  iswun  9103  elgrug  9191  iccshftr  11683  iccshftl  11685  iccdil  11687  icccntr  11689  fzaddel  11747  elfzomelpfzo  11914  axdc4uzlem  12092  wrdl1s1  12622  wwlktovf  12894  wwlktovf1  12895  wwlktovfo  12896  wrd2f1tovbij  12898  sqrmo  13085  resqrtcl  13087  resqrtthlem  13088  sqrtneg  13101  sqreu  13193  sqrtthlem  13195  eqsqrtd  13200  prodeq1f  13715  zprod  13744  divalglem10  14060  pythagtriplem18  14356  pythagtriplem19  14357  isstruct2  14641  imasval  14908  mreexexlemd  15041  catidd  15077  iscatd2  15078  subsubc  15222  isfunc  15233  funcres2b  15266  ispos  15576  posi  15579  isposd  15585  pospropd  15764  isps  15832  imasmnd2  15957  sgrp2rid2ex  16045  imasgrp2  16185  psgnunilem3  16521  isringd  17233  imasring  17268  isdrngd  17421  islmod  17516  lmodlema  17517  islmodd  17518  lmodprop2d  17572  lmhmpropd  17719  assapropd  17976  isphl  18663  isphld  18689  phlpropd  18690  mdetunilem3  19116  mdetunilem9  19122  fiinopn  19410  iscldtop  19596  lmfval  19733  consuba  19921  1stcfb  19946  2ndcctbss  19956  subislly  19982  ptval  20071  elpt  20073  elptr  20074  upxp  20124  isfbas  20330  ustval  20705  isust  20706  ustincl  20710  ustdiag  20711  ustinvel  20712  ustexhalf  20713  ust0  20722  imasdsf1olem  20876  lmhmclm  21586  iscph  21617  iscau2  21716  pmltpclem1  21860  isi1f  22081  mbfi1fseqlem6  22127  iblcnlem  22195  dvfsumlem4  22430  aannenlem1  22724  aannenlem2  22725  ulmval  22775  istrkgb  23852  istrkge  23854  istrkg2d  23856  istrkgld  23857  istrkg2ld  23858  axtgupdim2  23869  axtgeucl  23870  trgcgrg  23906  ishlg  23986  colline  24030  iscgra  24169  brbtwn  24202  axpaschlem  24243  axlowdim  24264  axeuclid  24266  eengtrkge  24289  nb3grapr  24453  nb3grapr2  24454  cusgra3v  24464  wlks  24519  iswlk  24520  wlkcompim  24526  wlkelwrd  24530  iswlkon  24534  istrl  24539  wlkntrl  24564  is2wlk  24567  ispth  24570  2pthoncl  24605  usg2wlk  24617  3v3e3cycl1  24644  constr3trllem5  24654  constr3cyclpe  24663  4cycl4dv4e  24668  wlkiswwlk2  24697  wwlkextfun  24729  wwlkextinj  24730  wwlkextbij  24733  wwlkextprop  24744  clwlkisclwwlklem2  24786  erclwwlkeq  24811  erclwwlkneq  24823  el2wlkonot  24869  el2spthonot  24870  el2spthonot0  24871  iseupa  24965  eupa0  24974  eupares  24975  eupap1  24976  frgra3v  25002  3cyclfrgrarn1  25012  2spotdisj  25061  numclwlk1lem2foa  25091  isplig  25179  lpni  25181  isgrpo  25198  isgrpda  25299  isass  25318  ismndo2  25347  isrngo  25380  rngomndo  25423  vci  25441  isvclem  25470  isnvlem  25503  sspval  25636  isssp  25637  ajfval  25724  dipdir  25757  siilem2  25767  issh  26125  elunop2  26932  superpos  27273  resspos  27647  isslmd  27745  slmdlema  27746  locfinreflem  27843  locfinref  27844  zhmnrg  27948  ismntoplly  28003  issiga  28111  isrnsigaOLD  28112  isrnsiga  28113  ismeas  28170  isrnmeas  28171  afsval  28551  brafs  28552  cvmlift3lem2  28765  cvmlift3lem6  28769  cvmlift3lem7  28770  cvmlift3lem9  28772  cvmlift3  28773  mclsppslem  28943  dfrtrcl2  29071  dfon2lem1  29215  dfon2lem3  29217  dfon2lem7  29221  wfrlem1  29343  wfrlem15  29357  frrlem1  29387  nodense  29449  brofs  29655  ofscom  29657  btwnouttr  29674  brifs  29693  cgr3com  29703  brcolinear  29709  brfs  29729  mblfinlem3  30053  indexa  30224  sdclem1  30236  fdc  30238  neificl  30246  heiborlem2  30308  igenval2  30463  ismrc  30633  rabren3dioph  30749  irrapxlem5  30762  rmydioph  30956  mpaaeu  31099  mpaaval  31100  mpaalem  31101  eliooshift  31541  stoweidlem5  31787  stoweidlem18  31800  stoweidlem28  31810  stoweidlem31  31813  stoweidlem41  31823  stoweidlem43  31825  stoweidlem44  31826  stoweidlem45  31827  stoweidlem51  31833  stoweidlem55  31837  stoweidlem59  31841  usgra2pthspth  32351  el0ldep  33067  ldepspr  33074  lmod1  33093  zlmodzxzldep  33105  bnj919  33825  bnj976  33836  bnj607  33974  bnj873  33982  lshpset2N  34844  isopos  34905  oposlem  34907  cmtfvalN  34935  cvrfval  34993  3dimlem1  35182  3dim1lem5  35190  lplni2  35261  lvoli2  35305  4atlem11  35333  dalawlem15  35609  cdlemftr3  36291  tendofset  36484  tendoset  36485  istendo  36486  cdlemk28-3  36634  cdlemkid3N  36659  cdlemkid4  36660  lpolsetN  37209  islpolN  37210  lpolconN  37214
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 185  df-an 371  df-3an 975
  Copyright terms: Public domain W3C validator