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

Theorem 3jca 1135
Description: Join consequents with conjunction. (Contributed by NM, 9-Apr-1994.)
Hypotheses
Ref Expression
3jca.1  |-  ( ph  ->  ps )
3jca.2  |-  ( ph  ->  ch )
3jca.3  |-  ( ph  ->  th )
Assertion
Ref Expression
3jca  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )

Proof of Theorem 3jca
StepHypRef Expression
1 3jca.1 . . 3  |-  ( ph  ->  ps )
2 3jca.2 . . 3  |-  ( ph  ->  ch )
3 3jca.3 . . 3  |-  ( ph  ->  th )
41, 2, 3jca31 522 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  /\  th )
)
5 df-3an 939 . 2  |-  ( ( ps  /\  ch  /\  th )  <->  ( ( ps 
/\  ch )  /\  th ) )
64, 5sylibr 205 1  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360    /\ w3a 937
This theorem is referenced by:  3jcad  1136  mpbir3and  1138  syl3anbrc  1139  3anim123i  1140  syl3anc  1185  syl13anc  1187  syl31anc  1188  syl113anc  1197  syl131anc  1198  syl311anc  1199  syl33anc  1200  syl133anc  1208  syl313anc  1209  syl331anc  1210  syl333anc  1217  3jaob  1247  mp3and  1283  soltmin  5276  tz7.49  6705  oeeulem  6847  domss2  7269  intrnfi  7424  dffi2  7431  elfiun  7438  hartogslem1  7514  wemaplem2  7519  oemapvali  7643  cfss  8150  cofsmo  8154  axdc3lem4  8338  axdc4lem  8340  fpwwe2lem6  8515  fpwwe2lem13  8522  canth4  8527  intwun  8615  r1limwun  8616  wunex2  8618  tskwun  8664  gruwun  8693  intgru  8694  wfgru  8696  grutsk1  8701  le2tri3i  9208  ledivmulOLD  9889  supmul1  9978  supmullem2  9980  eluzp1p1  10516  peano2uz  10535  rpnnen1lem5  10609  ixxun  10937  elioc2  10978  elico2  10979  elicc2  10980  iccsupr  11002  iccsplit  11034  fzrev3  11116  fseq1p1m1  11127  elfzo2  11148  elfzo0  11176  elfzo1  11178  elfznelfzo  11197  intfrac2  11244  intfracq  11245  seqf1olem2  11368  hashprb  11673  brfi1uzind  11720  remullem  11938  sqr0lem  12051  sqrlem3  12055  resqreu  12063  resqrcl  12064  sqrneglem  12077  sqreulem  12168  eqsqrd  12176  climsup  12468  fsumcvg3  12528  supcvg  12640  mertenslem2  12667  sin02gt0  12798  ruclem1  12835  ruclem2  12836  ruclem11  12844  gcdcllem3  13018  rppwr  13062  qredeq  13111  maxprmfct  13118  pythagtriplem6  13200  pythagtriplem7  13201  pythagtriplem19  13212  pclem  13217  prmreclem1  13289  ramcl  13402  iscatd2  13911  issubc3  14051  prsref  14394  posref  14413  isposd  14417  isposi  14418  latjlej1  14499  latmlem1  14515  latledi  14523  latj32  14531  mod2ile  14540  lubss  14553  pslem  14643  letsr  14677  0mhm  14763  resmhm  14764  resmhm2  14765  resmhm2b  14766  mhmco  14767  prdspjmhm  14771  pwsdiagmhm  14773  pwsco1mhm  14774  pwsco2mhm  14775  frmdup1  14814  grpinvid1  14858  grpinvid2  14859  grplcan  14862  issubg2  14964  issubg4  14966  ghmmhm  15021  cayley  15117  lsmelvali  15289  pj1id  15336  frgpmhm  15402  mulgmhm  15455  dmdprdsplit  15610  ablfac1lem  15631  ablfac2  15652  rnglz  15705  rngrz  15706  isrhm2d  15834  subrgunit  15891  issubrg2  15893  islmodd  15961  islmhm2  16119  islmhmd  16120  reslmhm  16133  islbs2  16231  islbs3  16232  isassad  16387  isphld  16890  iscldtop  17164  neiptoptop  17200  iscnp2  17308  cnpnei  17333  cnpco  17336  hausnei2  17422  nconsubb  17491  nlly2i  17544  elptr  17610  upxp  17660  elmptrab2  17865  opnfbas  17879  isfil2  17893  isfild  17895  infil  17900  fsubbas  17904  neifil  17917  fbasrn  17921  rnelfmlem  17989  fmfnfmlem4  17994  fmfnfm  17995  flimclslem  18021  flimsncls  18023  istgp2  18126  tsmsfbas  18162  ustfilxp  18247  trust  18264  ustuqtop4  18279  tuslem  18302  tmslem  18517  stdbdmopn  18553  metustexhalfOLD  18598  metustexhalf  18599  metustfbasOLD  18600  metustfbas  18601  metustOLD  18602  metust  18603  isngp4  18663  sranlm  18725  nlmtlm  18734  lssnlm  18741  nmoleub  18770  qdensere  18809  iirev  18959  iihalf1  18961  iihalf2  18963  iimulcl  18967  icoopnst  18969  iocopnst  18970  evth  18989  pcoptcl  19051  pcorevcl  19055  nmhmcn  19133  cphsubrglem  19145  tchcph  19199  cmetcaulem  19246  hlprlem  19326  minveclem1  19330  minveclem3b  19334  ivthlem2  19354  ivthlem3  19355  vitalilem2  19506  mbfsup  19559  i1fd  19576  itg2seq  19637  itg2mono  19648  itgsplitioo  19732  dvfsumlem4  19918  dvfsumrlim3  19922  evlslem1  19941  mdegaddle  20002  mdegmullem  20006  ply1divmo  20063  ply1remlem  20090  fta1b  20097  plyremlem  20226  aannenlem2  20251  aalioulem5  20258  aalioulem6  20259  aaliou  20260  aaliou3lem3  20266  psercnlem2  20345  psercnlem1  20346  pserdvlem1  20348  ptolemy  20409  quart1cl  20699  quartlem2  20703  quartlem3  20704  quartlem4  20705  jensenlem2  20831  emcllem7  20845  ftalem4  20863  basellem2  20869  perfectlem1  21018  dchrelbasd  21028  dchrmulcl  21038  dchrinv  21050  lgsdchr  21137  pntlemd  21293  pntlemc  21294  pntlemb  21296  pntlemg  21297  usgra2edg  21407  wlkbprop  21539  wlkonwlk  21540  spthispth  21578  pthdepisspth  21579  isspthonpth  21589  1pthon  21596  constr2trl  21604  2pthon  21607  wlkdvspthlem  21612  wlkdvspth  21613  cyclispthon  21625  fargshiftf1  21629  constr3lem4  21639  constr3lem5  21640  constr3trllem1  21642  constr3trllem2  21643  constr3trl  21651  constr3pth  21652  constr3cyclp  21654  4cycl4dv  21659  vdgr0  21676  vdusgraval  21683  vdgrnn0pnf  21685  eupatrl  21695  grpoidinvlem2  21798  grpoidval  21809  grpoidinv2  21811  grpoinv  21820  grpoinvid1  21823  grpoinvid2  21824  grpolcan  21826  grpo2inv  21832  grpomuldivass  21842  grponpncan  21848  ablo4  21880  ablodivdiv4  21884  ablonnncan  21886  ablonnncan1  21888  ismndo1  21937  isrngod  21972  rngolz  21994  rngorz  21995  cnrngo  21996  vc0  22053  vcoprne  22063  isnvi  22097  nvmdi  22136  nvsubadd  22141  nvnpcan  22146  nvmeq0  22150  nvabs  22167  sspg  22232  ssps  22234  lno0  22262  nmoub3i  22279  nmblolbii  22305  ubthlem1  22377  minvecolem1  22381  elunop2  23521  pjclem4  23707  pj3si  23715  stlei  23748  csmdsymi  23842  atexch  23889  atcvatlem  23893  atcvat4i  23905  cdj3i  23949  iocinioc2  24147  xrstos  24206  ofldsqr  24245  ofldchr  24249  unitdivcld  24304  rnlogblem  24404  esumpcvgval  24473  pwsiga  24518  prsiga  24519  sigainb  24524  insiga  24525  isrnmeas  24559  measres  24581  measdivcstOLD  24583  measdivcst  24584  imambfm  24617  dya2iocnrect  24636  sibf0  24654  sibfof  24659  ballotlemsup  24767  subfacp1lem1  24870  subfacp1lem2a  24871  iccllyscon  24942  cvmsi  24957  cvmlift2lem10  25004  relexpindlem  25144  fprodeq0  25304  poseq  25533  wfrlem15  25557  elno2  25614  brbtwn2  25849  colinearalg  25854  ax5seg  25882  axlowdim  25905  axcontlem2  25909  axcontlem4  25911  axcontlem9  25916  axcontlem10  25917  axcontlem12  25919  5segofs  25945  cgrextend  25947  segconeq  25949  segconeu  25950  trisegint  25967  fvtransport  25971  ifscgr  25983  cgrxfr  25994  btwnxfr  25995  lineext  26015  brofs2  26016  brifs2  26017  linecgr  26020  lineid  26022  btwnconn1lem4  26029  btwnconn1lem7  26032  btwnconn1lem8  26033  btwnconn1lem9  26034  btwnconn1lem11  26036  btwnconn1lem12  26037  btwnconn1lem13  26038  btwnconn1lem14  26039  btwnconn3  26042  brsegle2  26048  broutsideof2  26061  btwnoutside  26064  broutsideof3  26065  outsideoftr  26068  outsideofeu  26070  liness  26084  lineunray  26086  ellines  26091  supaddc  26245  supadd  26246  mblfinlem3  26257  ismblfin  26259  itg2addnclem2  26271  ftc1anclem7  26300  ftc1anc  26302  tailfb  26420  indexa  26449  seqpo  26465  nninfnub  26469  sstotbnd2  26497  rngohomsub  26603  crngm4  26627  igenval2  26690  prnc  26691  isfldidl  26692  ismrc  26769  jm2.17a  27039  congabseq  27053  jm2.18  27073  jm2.26a  27085  jm2.26lem3  27086  jm2.16nn0  27089  jm2.27c  27092  pmtrfrn  27391  pmtrfb  27397  psgnunilem2  27409  psgnunilem3  27410  deg1mhm  27517  pm13.194  27603  ubelsupr  27681  cncmpmax  27693  rfcnpre3  27694  rfcnpre4  27695  fmuldfeq  27703  fmul01lt1lem1  27704  fmul01lt1lem2  27705  climinf  27722  stoweidlem3  27742  stoweidlem14  27753  stoweidlem15  27754  stoweidlem20  27759  stoweidlem23  27762  stoweidlem26  27765  stoweidlem29  27768  stoweidlem34  27773  stoweidlem38  27777  stoweidlem39  27778  stoweidlem43  27782  stoweidlem44  27783  stoweidlem50  27789  stoweidlem51  27790  stoweidlem56  27795  stoweidlem59  27798  sigarcol  27844  sharhght  27845  cevathlem2  27848  cevath  27849  ndmaovdistr  28061  el2xptp0  28076  oteqimp  28078  2leaddle2  28115  elfzmlbm  28129  elfzmlbp  28130  elfzelfzelfz  28132  elfz0fzfz0  28137  fz0fzelfz0  28141  fz0fzdiffz0  28142  ubmelfzo  28149  ubmelm1fzo  28150  fzo1fzo0n0  28151  subsubelfzo0  28158  fzofzim  28159  fzoopth  28162  2ffzoeq  28163  nn0nndivcl  28164  nn0ge0div  28165  flltdivnn0lt  28170  2submod  28175  wrdlenge2n0  28208  swrd0  28217  swrdvalodm2  28222  swrd0swrd  28231  swrdswrdlem  28232  swrd0swrdid  28234  swrdswrd0  28235  swrdccatin1  28239  swrdccatin12lem3a  28242  swrdccatin12lem3b  28243  swrdccatin2  28244  swrdccatin12lem3c  28245  swrdccatin12lem3  28246  swrdccatin12lem4  28247  swrdccatin12  28248  swrdccat3  28249  swrdccat  28250  modprm0  28262  cshwoor  28271  cshwidx  28276  cshwidxmod  28277  cshwidxn  28281  2cshw1lem1  28282  2cshw1lem2  28283  2cshw1lem3  28284  2cshw2lem1  28286  2cshw2lem2  28287  2cshw2lem3  28288  2cshwid  28292  swrdtrcfvl  28299  cshweqdif2  28304  cshweqdif2s  28305  2wlkeq  28341  usgra2pthspth  28343  usgra2wlkspth  28346  usgra2pthlem1  28348  usgra2pth  28349  usgra2adedgspth  28353  usgra2adedgwlk  28354  usgra2adedgwlkon  28355  wwlkn0  28371  wlkiswwlk1  28372  wlkiswwlk2lem6  28378  wlkiswwlk2  28379  wlklniswwlkn1  28381  el2wlkonot  28401  el2spthonot  28402  el2spthonot0  28403  el2wlkonotot0  28404  2wlkonot3v  28407  2spthonot3v  28408  usg2wotspth  28416  usg2spthonot0  28421  usg2spthonot1  28422  usgfidegfi  28425  3vfriswmgra  28469  2pthfrgra  28475  3cyclfrgra  28479  frgranbnb  28484  vdn0frgrav2  28488  vdn1frgrav2  28490  vdgfrgragt2  28492  frgrancvvdeqlem3  28495  frgrancvvdeqlemC  28502  frgrancvvdeq  28505  frgrawopreglem5  28511  frgrawopreg  28512  frg2woteu  28518  frg2woteqm  28522  frg2woteq  28523  usg2spot2nb  28528  usgreg2spot  28530  4animp1  28654  bnj951  29220  bnj605  29352  bnj607  29361  bnj908  29376  bnj1001  29403  bnj1110  29425  bnj1128  29433  islshpcv  29925  isopiN  30053  latm12  30102  omllaw5N  30119  cmtcomlemN  30120  cmtbr3N  30126  omlfh3N  30131  atlen0  30182  cvlsupr2  30215  hlomcmat  30236  exatleN  30275  2llnneN  30280  cvrexchlem  30290  cvratlem  30292  atcvrj2b  30303  atltcvr  30306  atlelt  30309  atexchcvrN  30311  cvrat4  30314  2atjm  30316  atbtwnexOLDN  30318  atbtwnex  30319  4noncolr3  30324  3dimlem2  30330  3dimlem3  30332  3dimlem3OLDN  30333  3dimlem4  30335  3dimlem4OLDN  30336  3dim1  30338  3dim2  30339  3dim3  30340  1cvrat  30347  ps-2b  30353  3atlem4  30357  3atlem5  30358  3atlem6  30359  llnexatN  30392  llncvrlpln2  30428  2llnmj  30431  lplnexatN  30434  4atlem3a  30468  4atlem10  30477  4atlem11b  30479  4atlem11  30480  4atlem12b  30482  4atlem12  30483  lplncvrlvol2  30486  2lplnja  30490  2lplnj  30491  2lplnmj  30493  dalemswapyz  30527  dalemrot  30528  dalemswapyzps  30561  dalemrotps  30562  dalem51  30594  dalem52  30595  dath2  30608  lneq2at  30649  lncvrelatN  30652  cdlema1N  30662  cdlema2N  30663  cdlemblem  30664  paddval  30669  padd01  30682  padd02  30683  paddss12  30690  paddasslem2  30692  paddasslem4  30694  paddasslem6  30696  paddasslem9  30699  paddasslem10  30700  paddasslem12  30702  paddasslem15  30705  pmodlem1  30717  pmod2iN  30720  pmodN  30721  pmapjat1  30724  dalawlem1  30742  paddunN  30798  poml4N  30824  poml5N  30825  osumcllem6N  30832  pexmidlem6N  30846  pl42lem2N  30851  lhpexle1lem  30878  lhpexle1  30879  lhpexle2lem  30880  lhpexle3lem  30882  lhpmcvr5N  30898  lhpmcvr6N  30899  4atexlemswapqr  30934  4atexlemex6  30945  cdlemd2  31070  cdlemd5  31073  cdleme01N  31092  cdleme3b  31100  cdleme20i  31188  cdleme20m  31194  cdleme21d  31201  cdleme21e  31202  cdleme21i  31206  cdleme21j  31207  cdleme21  31208  cdleme22cN  31213  cdleme22f2  31218  cdleme24  31223  cdleme26f2ALTN  31235  cdleme26f2  31236  cdleme27a  31238  cdleme28a  31241  cdleme43fsv1snlem  31291  cdleme37m  31333  cdleme38m  31334  cdleme38n  31335  cdleme40n  31339  cdleme42mgN  31359  cdleme46f2g2  31364  cdleme46f2g1  31365  cdlemf1  31432  cdlemftr2  31437  cdlemg17pq  31543  cdlemg29  31576  cdlemg33b  31578  cdlemi  31691  tendocan  31695  cdlemk6  31708  cdlemk7  31719  cdlemk12  31721  cdlemk16  31728  cdlemk5u  31732  cdlemk18  31739  cdlemk19  31740  cdlemk7u  31741  cdlemk11u  31742  cdlemk12u  31743  cdlemk21N  31744  cdlemk20  31745  cdlemk7u-2N  31759  cdlemk11u-2N  31760  cdlemk12u-2N  31761  cdlemk21-2N  31762  cdlemk20-2N  31763  cdlemk22  31764  cdlemk31  31767  cdlemk23-3  31773  cdlemk24-3  31774  cdlemk25-3  31775  cdlemk26b-3  31776  cdlemk26-3  31777  cdlemk27-3  31778  cdlemk28-3  31779  cdlemk33N  31780  cdlemk34  31781  cdlemky  31797  cdlemk11ta  31800  cdlemk19ylem  31801  cdlemk35s-id  31809  cdlemk39s-id  31811  cdlemk19xlem  31813  cdlemk11tc  31816  cdlemk11t  31817  cdlemk47  31820  cdlemk53b  31827  cdlemk53  31828  cdlemkyyN  31833  cdlemk55u1  31836  cdlemk19u1  31840  erng1r  31866  dvalveclem  31897  diclspsn  32066  dihmeetlem20N  32198  islpoldN  32356  lpolconN  32359
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 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator