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

Theorem 3jca 1176
Description: Join consequents with conjunction. (Contributed by NM, 9-Apr-1994.)
Hypotheses
Ref Expression
3jca.1
3jca.2
3jca.3
Assertion
Ref Expression
3jca

Proof of Theorem 3jca
StepHypRef Expression
1 3jca.1 . . 3
2 3jca.2 . . 3
3 3jca.3 . . 3
41, 2, 3jca31 534 . 2
5 df-3an 975 . 2
64, 5sylibr 212 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  3jcad  1177  mpbir3and  1179  syl3anbrc  1180  3anim123i  1181  syl3anc  1228  syl13anc  1230  syl31anc  1231  syl113anc  1240  syl131anc  1241  syl311anc  1242  syl33anc  1243  syl133anc  1251  syl313anc  1252  syl331anc  1253  syl333anc  1260  3jaob  1290  mp3and  1327  soltmin  5411  f1dom3fv3dif  6175  f1dom3el3dif  6176  oteqimp  6819  el2xptp0  6844  funsssuppss  6945  tz7.49  7129  oeeulem  7269  domss2  7696  intrnfi  7896  dffi2  7903  elfiun  7910  hartogslem1  7988  wemaplem2  7993  oemapvali  8124  cfss  8666  cofsmo  8670  axdc3lem4  8854  axdc4lem  8856  fpwwe2lem6  9034  fpwwe2lem13  9041  canth4  9046  intwun  9134  r1limwun  9135  wunex2  9137  tskwun  9183  gruwun  9212  intgru  9213  wfgru  9215  grutsk1  9220  le2tri3i  9735  ledivmulOLD  10444  supmul1  10533  supmullem2  10535  nn0ge2m1nn  10886  nn0nndivcl  10888  nn0ge0div  10957  eluzp1p1  11135  peano2uz  11163  rpnnen1lem5  11241  ixxun  11574  elioc2  11616  elico2  11617  elicc2  11618  iccsupr  11646  iccsplit  11682  uzsubsubfz  11736  fzrev3  11774  elfz1b  11777  fseq1p1m1  11781  elfz0ubfz0  11807  elfz0fzfz0  11808  fz0fzelfz0  11809  fz0fzdiffz0  11812  elfzmlbmOLD  11814  elfzmlbp  11815  elfzo2  11832  elfzo0  11863  fzo1fzo0n0  11864  elfzo0z  11865  fzofzim  11869  elfzo1  11871  ubmelfzo  11881  elfzodifsumelfzo  11882  elfzom1elp1fzo  11883  fzossfzop1  11893  ssfzo12bi  11907  elfznelfzo  11915  flltdivnn0lt  11965  intfrac2  11985  intfracq  11986  modltm1p1mod  12039  2submod  12048  suppssfz  12100  mptnn0fsuppr  12105  seqf1olem2  12147  hashprb  12462  hashprdifel  12463  hashge2el2dif  12521  brfi1uzind  12532  wrdlenge2n0  12577  lswcl  12589  ccatsymb  12600  wrdl1s1  12622  swrdvalodm2  12664  swrdeq  12671  swrdspsleq  12673  swrdswrdlem  12684  swrdswrd0  12687  swrdccatwrd  12693  swrdccatin1  12708  swrdccatin12lem2a  12710  swrdccatin12lem2b  12711  swrdccatin2  12712  swrdccatin12lem2c  12713  swrdccatin12lem2  12714  swrdccatin12lem3  12715  swrdccatin12  12716  swrdccat3  12717  swrdccat  12718  repswswrd  12756  repswccat  12757  cshwidxmod  12774  cshwidxn  12779  cshweqdif2  12787  cshwcshid  12795  swrdco  12803  swrd2lsw  12890  2swrd2eqwrdeq  12891  wwlktovfo  12896  remullem  12961  sqr0lem  13074  sqrlem3  13078  resqreu  13086  resqrtcl  13087  sqrtneglem  13100  sqreulem  13192  eqsqrtd  13200  climsup  13492  fsumcvg3  13551  modfsummods  13607  supcvg  13667  mertenslem2  13694  fprodeq0  13779  sin02gt0  13927  ruclem1  13964  ruclem2  13965  ruclem11  13973  gcdcllem3  14151  rppwr  14195  qredeq  14247  maxprmfct  14254  modprm0  14330  pythagtriplem6  14345  pythagtriplem7  14346  pythagtriplem19  14357  pclem  14362  prmreclem1  14434  ramcl  14547  cshwsidrepsw  14578  iscatd2  15078  issubc3  15218  prsref  15561  posrefOLD  15581  isposd  15585  isposi  15586  latjlej1  15695  latmlem1  15711  latledi  15719  latj32  15727  mod2ile  15736  lubss  15751  pslem  15836  letsr  15857  idmhm  15975  mhmf1o  15976  0mhm  15989  resmhm  15990  resmhm2  15991  resmhm2b  15992  mhmco  15993  prdspjmhm  15998  pwsdiagmhm  16000  pwsco1mhm  16001  pwsco2mhm  16002  frmdup1  16032  mgm2nsgrplem4  16039  sgrp2rid2ex  16045  grpinvid1  16098  grpinvid2  16099  grplcan  16102  mhmfmhm  16193  issubg2  16216  issubg4  16220  ghmmhm  16277  cayley  16439  gsmsymgrfixlem1  16452  fvcosymgeq  16454  gsmsymgreqlem1  16455  gsmsymgreqlem2  16456  pmtrfrn  16483  pmtrfb  16490  pmtr3ncomlem1  16498  psgnunilem2  16520  psgnunilem3  16521  lsmelvali  16670  pj1id  16717  frgpmhm  16783  mulgmhm  16836  fsfnn0gsumfsffz  17011  dprdvalOLD  17036  dmdprdsplit  17096  ablfac1lem  17119  ablfac2  17140  srglmhm  17186  srgrmhm  17187  srgbinomlem  17195  ringlz  17235  ringrz  17236  crngbinom  17270  isrhm2d  17377  subrgunit  17447  issubrg2  17449  islmodd  17518  islmhm2  17684  islmhmd  17685  reslmhm  17698  islbs2  17800  islbs3  17801  isassad  17972  evlslem1  18184  cply1coe0bi  18342  gsummoncoe1  18346  psgndiflemB  18636  psgndif  18638  isphld  18689  frlmbas  18786  mat1mhm  18986  dmatmul  18999  dmatsubcl  19000  dmatscmcl  19005  scmatscmiddistr  19010  scmatmats  19013  scmatmhm  19036  mavmulsolcl  19053  ma1repveval  19073  mulmarep1gsum2  19076  1marepvmarrepid  19077  1marepvsma1  19085  m1detdiag  19099  mdetdiagid  19102  mdetunilem6  19119  mdetunilem8  19121  minmar1cl  19153  gsummatr01lem4  19160  slesolvec  19181  cramerimplem2  19186  cramerimp  19188  cpmatinvcl  19218  mat2pmat1  19233  mat2pmatmhm  19234  d1mat2pmat  19240  decpmatmul  19273  pmatcollpw2lem  19278  pmatcollpw2  19279  pmatcollpwscmatlem2  19291  mp2pm2mp  19312  pm2mpmhmlem2  19320  pm2mpmhm  19321  chmatval  19330  chpmat1dlem  19336  chpdmatlem2  19340  chpdmat  19342  chpscmatgsummon  19346  chpidmat  19348  chfacfscmulgsum  19361  chfacfpmmulgsum  19365  chfacfpmmulgsum2  19366  iscldtop  19596  neiptoptop  19632  iscnp2  19740  cnpnei  19765  cnpco  19768  hausnei2  19854  nconsubb  19924  nlly2i  19977  lfinun  20026  elptr  20074  upxp  20124  elmptrab2  20329  opnfbas  20343  isfil2  20357  isfild  20359  infil  20364  fsubbas  20368  neifil  20381  fbasrn  20385  rnelfmlem  20453  fmfnfmlem4  20458  fmfnfm  20459  flimclslem  20485  flimsncls  20487  istgp2  20590  tsmsfbas  20626  ustfilxp  20715  trust  20732  ustuqtop4  20747  tuslem  20770  tmslem  20985  stdbdmopn  21021  metustexhalfOLD  21066  metustexhalf  21067  metustfbasOLD  21068  metustfbas  21069  metustOLD  21070  metust  21071  isngp4  21131  sranlm  21193  nlmtlm  21202  lssnlm  21209  nmoleub  21238  qdensere  21277  iirev  21429  iihalf1  21431  iihalf2  21433  iimulcl  21437  icoopnst  21439  iocopnst  21440  evth  21459  pcoptcl  21521  pcorevcl  21525  nmhmcn  21603  cphsubrglem  21624  tchcph  21680  cmetcaulem  21727  hlprlem  21807  minveclem1  21839  minveclem3b  21843  ivthlem2  21864  ivthlem3  21865  vitalilem2  22018  mbfsup  22071  i1fd  22088  itg2seq  22149  itg2mono  22160  itgsplitioo  22244  dvfsumlem4  22430  dvfsumrlim3  22434  mdegaddle  22474  mdegmullem  22478  ply1divmo  22536  ply1remlem  22563  fta1b  22570  plyremlem  22700  aannenlem2  22725  aalioulem5  22732  aalioulem6  22733  aaliou  22734  aaliou3lem3  22740  psercnlem2  22819  psercnlem1  22820  pserdvlem1  22822  ptolemy  22889  quart1cl  23185  quartlem2  23189  quartlem3  23190  quartlem4  23191  jensenlem2  23317  emcllem7  23331  ftalem4  23349  basellem2  23355  perfectlem1  23504  dchrelbasd  23514  dchrmulcl  23524  dchrinv  23536  lgsdchr  23623  pntlemd  23779  pntlemc  23780  pntlemb  23782  pntlemg  23783  axtg5seg  23862  axtgupdim2  23869  trgcgrg  23906  hlid  23993  hltr  23994  btwnhl1  23996  btwnhl2  23997  mirhl  24059  mirbtwnhl  24060  lnopp2hpgb  24132  f1otrg  24174  brbtwn2  24208  colinearalg  24213  ax5seg  24241  axlowdim  24264  axcontlem2  24268  axcontlem4  24270  axcontlem9  24275  axcontlem10  24276  axcontlem12  24278  eengtrkg  24288  usgra2edg  24382  wlkbprop  24523  wlkonwlk  24537  spthispth  24575  pthdepisspth  24576  isspthonpth  24586  1pthon  24593  constr2trl  24601  2pthon  24604  wlkdvspthlem  24609  wlkdvspth  24610  usgra2adedgspth  24613  usgra2adedgwlk  24614  usgra2adedgwlkon  24615  usgra2adedgwlkonALT  24616  usgra2wlkspth  24621  cyclispthon  24633  fargshiftf1  24637  constr3lem4  24647  constr3lem5  24648  constr3trllem1  24650  constr3trllem2  24651  constr3trl  24659  constr3pth  24660  constr3cyclp  24662  4cycl4dv  24667  wwlkn0  24689  wlkiswwlk1  24690  wlkiswwlk2lem6  24696  wlkiswwlk2  24697  wlklniswwlkn1  24699  wwlkn0s  24705  vfwlkniswwlkn  24706  2wlkeq  24707  wwlknred  24723  wwlknext  24724  wwlknredwwlkn  24726  wwlknredwwlkn0  24727  wwlkm1edg  24735  wwlkextproplem1  24741  wwlkextproplem2  24742  clwwlkn0  24774  clwwlknimp  24776  clwlkisclwwlklem2a4  24784  clwlkisclwwlklem2a  24785  clwlkisclwwlklem1  24787  clwwlkel  24793  clwwlkf  24794  clwwlkf1  24796  clwwlknwwlkncl  24800  clwwlkext2edg  24802  wwlkext2clwwlk  24803  wwlksubclwwlk  24804  clwwisshclww  24807  erclwwlksym  24814  erclwwlktr  24815  eleclclwwlknlem1  24817  usg2cwwkdifex  24821  erclwwlknsym  24826  erclwwlkntr  24827  hashecclwwlkn1  24834  usghashecclwwlk  24835  clwlkfclwwlk  24844  clwlkf1clwwlklem  24849  el2wlkonot  24869  el2spthonot  24870  el2spthonot0  24871  el2wlkonotot0  24872  2wlkonot3v  24875  2spthonot3v  24876  usg2wotspth  24884  usg2spthonot0  24889  usg2spthonot1  24890  vdgr0  24900  vdusgraval  24907  vdgrnn0pnf  24909  usgfidegfi  24910  rusgraprop2  24942  rusgraprop3  24943  rusgraprop4  24944  rusgra0edg  24955  eupatrl  24968  3vfriswmgra  25005  2pthfrgra  25011  3cyclfrgra  25015  frgranbnb  25020  vdn0frgrav2  25023  vdn1frgrav2  25025  vdgfrgragt2  25027  frgrancvvdeqlem3  25032  frgrancvvdeqlemC  25039  frgrancvvdeq  25042  frgrawopreglem5  25048  frgrawopreg  25049  frg2woteu  25055  frg2woteqm  25059  frg2woteq  25060  usg2spot2nb  25065  usgreg2spot  25067  extwwlkfablem2  25078  numclwwlkovf2ex  25086  extwwlkfab  25090  numclwlk1lem2foa  25091  numclwlk1lem2f1  25094  numclwwlkqhash  25100  numclwwlk2lem1  25102  numclwwlk5  25112  numclwwlk7  25114  frgraogt3nreg  25120  friendship  25122  grpoidinvlem2  25207  grpoidval  25218  grpoidinv2  25220  grpoinv  25229  grpoinvid1  25232  grpoinvid2  25233  grpolcan  25235  grpo2inv  25241  grpomuldivass  25251  grponpncan  25257  ablo4  25289  ablodivdiv4  25293  ablonnncan  25295  ablonnncan1  25297  ismndo1  25346  isrngod  25381  rngolz  25403  rngorz  25404  cnrngo  25405  vc0  25462  vcoprne  25472  isnvi  25506  nvmdi  25545  nvsubadd  25550  nvnpcan  25555  nvmeq0  25559  nvabs  25576  sspg  25641  ssps  25643  lno0  25671  nmoub3i  25688  nmblolbii  25714  ubthlem1  25786  minvecolem1  25790  elunop2  26932  pjclem4  27118  pj3si  27126  stlei  27159  csmdsymi  27253  atexch  27300  atcvatlem  27304  atcvat4i  27316  cdj3i  27360  iocinioc2  27590  omndadd2d  27698  omndadd2rd  27699  omndmul2  27702  lmodslmd  27747  orngsqr  27794  ofldchr  27804  xrge0slmod  27834  unitdivcld  27883  rnlogblem  28015  esumpcvgval  28084  pwsiga  28130  prsiga  28131  sigainb  28136  insiga  28137  isrnmeas  28171  measres  28193  measdivcstOLD  28195  imambfm  28233  dya2iocnrect  28252  ballotlemsup  28443  subfacp1lem1  28623  subfacp1lem2a  28624  iccllyscon  28695  cvmsi  28710  cvmlift2lem10  28757  elmrsubrn  28880  mclsrcl  28921  relexpindlem  29062  poseq  29333  wfrlem15  29357  elno2  29414  5segofs  29656  cgrextend  29658  segconeq  29660  segconeu  29661  trisegint  29678  fvtransport  29682  ifscgr  29694  cgrxfr  29705  btwnxfr  29706  lineext  29726  brofs2  29727  brifs2  29728  linecgr  29731  lineid  29733  btwnconn1lem4  29740  btwnconn1lem7  29743  btwnconn1lem8  29744  btwnconn1lem9  29745  btwnconn1lem11  29747  btwnconn1lem12  29748  btwnconn1lem13  29749  btwnconn1lem14  29750  btwnconn3  29753  brsegle2  29759  broutsideof2  29772  btwnoutside  29775  broutsideof3  29776  outsideoftr  29779  outsideofeu  29781  liness  29795  lineunray  29797  ellines  29802  supaddc  30041  supadd  30042  mblfinlem3  30053  ismblfin  30055  itg2addnclem2  30067  ftc1anclem7  30096  ftc1anc  30098  tailfb  30195  indexa  30224  seqpo  30240  nninfnub  30244  sstotbnd2  30270  rngohomsub  30376  crngm4  30400  igenval2  30463  prnc  30464  isfldidl  30465  ismrc  30633  jm2.17a  30898  congabseq  30912  jm2.18  30930  jm2.26a  30942  jm2.26lem3  30943  jm2.16nn0  30946  jm2.27c  30949  deg1mhm  31167  ioounsn  31177  iocinico  31179  pm13.194  31319  ubelsupr  31395  cncmpmax  31407  rfcnpre3  31408  rfcnpre4  31409  monoords  31496  fzdifsuc2  31512  iccshift  31558  fmuldfeq  31577  fmul01lt1lem1  31578  fmul01lt1lem2  31579  mccllem  31605  climinf  31612  sumnnodd  31636  lptre2pt  31646  icccncfext  31690  dvnmptdivc  31735  dvdsn1add  31736  dvnmul  31740  dvmptfprodlem  31741  dvnprodlem1  31743  dvnprodlem2  31744  iblspltprt  31772  iblcncfioo  31777  itgspltprt  31778  itgperiod  31780  stoweidlem3  31785  stoweidlem14  31796  stoweidlem15  31797  stoweidlem23  31805  stoweidlem26  31808  stoweidlem29  31811  stoweidlem34  31816  stoweidlem38  31820  stoweidlem39  31821  stoweidlem43  31825  stoweidlem44  31826  stoweidlem50  31832  stoweidlem51  31833  stoweidlem56  31838  stoweidlem59  31841  fourierdlem11  31900  fourierdlem12  31901  fourierdlem14  31903  fourierdlem41  31930  fourierdlem42  31931  fourierdlem48  31937  fourierdlem49  31938  fourierdlem50  31939  fourierdlem79  31968  fourierdlem81  31970  fourierdlem92  31981  fourierdlem93  31982  fourierdlem102  31991  fourierdlem114  32003  elaa2lem  32016  etransclem3  32020  etransclem7  32024  etransclem10  32027  etransclem24  32041  etransclem25  32042  etransclem27  32044  etransclem28  32045  etransclem35  32052  etransclem38  32055  etransclem44  32061  sigarcol  32081  sharhght  32082  cevathlem2  32085  cevath  32086  ndmaovdistr  32292  cnambpcma  32315  2leaddle2  32320  eluzge0nn0  32329  elfzelfzlble  32337  subsubelfzo0  32338  fzoopth  32340  2ffzoeq  32341  usgra2pthspth  32351  usgra2pthlem1  32353  usgra2pth  32354  usgvad2edg  32411  equivestrcsetc  32658  c0mhm  32716  lidldomn1  32727  cznrng  32763  zrinitorngc  32808  zrtermorngc  32809  zrtermoringc  32878  scmsuppfi  32970  lcosn0  33021  lcoc0  33023  lincscmcl  33033  lindslinindsimp1  33058  lindslinindimp2lem4  33062  ldepspr  33074  lincresunit3lem3  33075  lincresunit2  33079  lincresunit3  33082  islindeps2  33084  isldepslvec2  33086  lmod1  33093  bnj951  33834  bnj605  33965  bnj607  33974  bnj908  33989  bnj1001  34016  bnj1110  34038  bnj1128  34046  islshpcv  34778  latm12  34955  omllaw5N  34972  cmtcomlemN  34973  cmtbr3N  34979  omlfh3N  34984  atlen0  35035  cvlsupr2  35068  hlomcmat  35089  exatleN  35128  2llnneN  35133  cvrexchlem  35143  cvratlem  35145  atcvrj2b  35156  atltcvr  35159  atlelt  35162  atexchcvrN  35164  cvrat4  35167  2atjm  35169  atbtwnexOLDN  35171  atbtwnex  35172  4noncolr3  35177  3dimlem2  35183  3dimlem3  35185  3dimlem3OLDN  35186  3dimlem4  35188  3dimlem4OLDN  35189  3dim1  35191  3dim2  35192  3dim3  35193  1cvrat  35200  ps-2b  35206  3atlem4  35210  3atlem5  35211  3atlem6  35212  llnexatN  35245  llncvrlpln2  35281  2llnmj  35284  lplnexatN  35287  4atlem3a  35321  4atlem10  35330  4atlem11b  35332  4atlem11  35333  4atlem12b  35335  4atlem12  35336  lplncvrlvol2  35339  2lplnja  35343  2lplnj  35344  2lplnmj  35346  dalemswapyz  35380  dalemrot  35381  dalemswapyzps  35414  dalemrotps  35415  dalem51  35447  dalem52  35448  dath2  35461  lneq2at  35502  lncvrelatN  35505  cdlema1N  35515  cdlema2N  35516  cdlemblem  35517  paddval  35522  padd01  35535  padd02  35536  paddss12  35543  paddasslem2  35545  paddasslem4  35547  paddasslem6  35549  paddasslem9  35552  paddasslem10  35553  paddasslem12  35555  paddasslem15  35558  pmodlem1  35570  pmod2iN  35573  pmodN  35574  pmapjat1  35577  dalawlem1  35595  paddunN  35651  poml4N  35677  poml5N  35678  osumcllem6N  35685  pexmidlem6N  35699  pl42lem2N  35704  lhpexle1lem  35731  lhpexle1  35732  lhpexle2lem  35733  lhpexle3lem  35735  lhpmcvr5N  35751  lhpmcvr6N  35752  4atexlemswapqr  35787  4atexlemex6  35798  cdlemd2  35924  cdlemd5  35927  cdleme01N  35946  cdleme3b  35954  cdleme20i  36043  cdleme20m  36049  cdleme21d  36056  cdleme21e  36057  cdleme21i  36061  cdleme21j  36062  cdleme21  36063  cdleme22cN  36068  cdleme22f2  36073  cdleme24  36078  cdleme26f2ALTN  36090  cdleme26f2  36091  cdleme27a  36093  cdleme28a  36096  cdleme43fsv1snlem  36146  cdleme37m  36188  cdleme38m  36189  cdleme38n  36190  cdleme40n  36194  cdleme42mgN  36214  cdleme46f2g2  36219  cdleme46f2g1  36220  cdlemf1  36287  cdlemftr2  36292  cdlemg17pq  36398  cdlemg29  36431  cdlemg33b  36433  cdlemi  36546  tendocan  36550  cdlemk6  36563  cdlemk7  36574  cdlemk12  36576  cdlemk16  36583  cdlemk5u  36587  cdlemk18  36594  cdlemk19  36595  cdlemk7u  36596  cdlemk11u  36597  cdlemk12u  36598  cdlemk21N  36599  cdlemk20  36600  cdlemk7u-2N  36614  cdlemk11u-2N  36615  cdlemk12u-2N  36616  cdlemk21-2N  36617  cdlemk20-2N  36618  cdlemk22  36619  cdlemk31  36622  cdlemk23-3  36628  cdlemk24-3  36629  cdlemk25-3  36630  cdlemk26b-3  36631  cdlemk26-3  36632  cdlemk27-3  36633  cdlemk28-3  36634  cdlemk33N  36635  cdlemk34  36636  cdlemky  36652  cdlemk11ta  36655  cdlemk19ylem  36656  cdlemk35s-id  36664  cdlemk39s-id  36666  cdlemk19xlem  36668  cdlemk11tc  36671  cdlemk11t  36672  cdlemk47  36675  cdlemk53b  36682  cdlemk53  36683  cdlemkyyN  36688  cdlemk55u1  36691  cdlemk19u1  36695  erng1r  36721  dvalveclem  36752  diclspsn  36921  dihmeetlem20N  37053  islpoldN  37211  lpolconN  37214  cotr2g  37786
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