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

Theorem 3jca 1134
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 521 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  /\  th )
)
5 df-3an 938 . 2  |-  ( ( ps  /\  ch  /\  th )  <->  ( ( ps 
/\  ch )  /\  th ) )
64, 5sylibr 204 1  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  3jcad  1135  mpbir3and  1137  syl3anbrc  1138  3anim123i  1139  syl3anc  1184  syl13anc  1186  syl31anc  1187  syl113anc  1196  syl131anc  1197  syl311anc  1198  syl33anc  1199  syl133anc  1207  syl313anc  1208  syl331anc  1209  syl333anc  1216  3jaob  1246  mp3and  1282  soltmin  5214  tz7.49  6639  oeeulem  6781  domss2  7203  intrnfi  7357  dffi2  7364  elfiun  7371  hartogslem1  7445  wemaplem2  7450  oemapvali  7574  cfss  8079  cofsmo  8083  axdc3lem4  8267  axdc4lem  8269  fpwwe2lem6  8444  fpwwe2lem13  8451  canth4  8456  intwun  8544  r1limwun  8545  wunex2  8547  tskwun  8593  gruwun  8622  intgru  8623  wfgru  8625  grutsk1  8630  le2tri3i  9136  ledivmulOLD  9817  supmul1  9906  supmullem2  9908  eluzp1p1  10444  peano2uz  10463  rpnnen1lem5  10537  ixxun  10865  elioc2  10906  elico2  10907  elicc2  10908  iccsupr  10930  iccsplit  10962  fzrev3  11043  fseq1p1m1  11053  elfzo2  11074  elfzo0  11102  elfznelfzo  11120  intfrac2  11167  intfracq  11168  seqf1olem2  11291  hashprb  11596  brfi1uzind  11643  remullem  11861  sqr0lem  11974  sqrlem3  11978  resqreu  11986  resqrcl  11987  sqrneglem  12000  sqreulem  12091  eqsqrd  12099  climsup  12391  fsumcvg3  12451  supcvg  12563  mertenslem2  12590  sin02gt0  12721  ruclem1  12758  ruclem2  12759  ruclem11  12767  gcdcllem3  12941  rppwr  12985  qredeq  13034  maxprmfct  13041  pythagtriplem6  13123  pythagtriplem7  13124  pythagtriplem19  13135  pclem  13140  prmreclem1  13212  ramcl  13325  iscatd2  13834  issubc3  13974  prsref  14317  posref  14336  isposd  14340  isposi  14341  latjlej1  14422  latmlem1  14438  latledi  14446  latj32  14454  mod2ile  14463  lubss  14476  pslem  14566  letsr  14600  0mhm  14686  resmhm  14687  resmhm2  14688  resmhm2b  14689  mhmco  14690  prdspjmhm  14694  pwsdiagmhm  14696  pwsco1mhm  14697  pwsco2mhm  14698  frmdup1  14737  grpinvid1  14781  grpinvid2  14782  grplcan  14785  issubg2  14887  issubg4  14889  ghmmhm  14944  cayley  15040  lsmelvali  15212  pj1id  15259  frgpmhm  15325  mulgmhm  15378  dmdprdsplit  15533  ablfac1lem  15554  ablfac2  15575  rnglz  15628  rngrz  15629  isrhm2d  15757  subrgunit  15814  issubrg2  15816  islmodd  15884  islmhm2  16042  islmhmd  16043  reslmhm  16056  islbs2  16154  islbs3  16155  isassad  16310  isphld  16809  iscldtop  17083  neiptoptop  17119  iscnp2  17226  cnpnei  17251  cnpco  17254  hausnei2  17340  nconsubb  17408  nlly2i  17461  elptr  17527  upxp  17577  elmptrab2  17782  opnfbas  17796  isfil2  17810  isfild  17812  infil  17817  fsubbas  17821  neifil  17834  fbasrn  17838  rnelfmlem  17906  fmfnfmlem4  17911  fmfnfm  17912  flimclslem  17938  flimsncls  17940  istgp2  18043  tsmsfbas  18079  ustfilxp  18164  trust  18181  ustuqtop4  18196  tuslem  18219  tmslem  18403  stdbdmopn  18439  metustexhalf  18477  metustfbas  18478  metust  18479  isngp4  18530  sranlm  18592  nlmtlm  18601  lssnlm  18608  nmoleub  18637  qdensere  18676  iirev  18826  iihalf1  18828  iihalf2  18830  iimulcl  18834  icoopnst  18836  iocopnst  18837  evth  18856  pcoptcl  18918  pcorevcl  18922  nmhmcn  19000  cphsubrglem  19012  tchcph  19066  cmetcaulem  19113  hlprlem  19189  minveclem1  19193  minveclem3b  19197  ivthlem2  19217  ivthlem3  19218  vitalilem2  19369  mbfsup  19424  i1fd  19441  itg2seq  19502  itg2mono  19513  itgsplitioo  19597  dvfsumlem4  19781  dvfsumrlim3  19785  evlslem1  19804  mdegaddle  19865  mdegmullem  19869  ply1divmo  19926  ply1remlem  19953  fta1b  19960  plyremlem  20089  aannenlem2  20114  aalioulem5  20121  aalioulem6  20122  aaliou  20123  aaliou3lem3  20129  psercnlem2  20208  psercnlem1  20209  pserdvlem1  20211  ptolemy  20272  quart1cl  20562  quartlem2  20566  quartlem3  20567  quartlem4  20568  jensenlem2  20694  emcllem7  20708  ftalem4  20726  basellem2  20732  perfectlem1  20881  dchrelbasd  20891  dchrmulcl  20901  dchrinv  20913  lgsdchr  21000  pntlemd  21156  pntlemc  21157  pntlemb  21159  pntlemg  21160  usgra2edg  21269  wlkbprop  21399  wlkonwlk  21400  spthispth  21428  pthdepisspth  21429  1pthon  21440  2pthon  21451  wlkdvspthlem  21456  wlkdvspth  21457  cyclispthon  21469  fargshiftf1  21473  constr3lem4  21483  constr3lem5  21484  constr3trllem1  21486  constr3trllem2  21487  constr3trl  21495  constr3pth  21496  constr3cyclp  21498  4cycl4dv  21503  vdgr0  21520  vdusgraval  21527  vdgrnn0pnf  21529  eupatrl  21539  grpoidinvlem2  21642  grpoidval  21653  grpoidinv2  21655  grpoinv  21664  grpoinvid1  21667  grpoinvid2  21668  grpolcan  21670  grpo2inv  21676  grpomuldivass  21686  grponpncan  21692  ablo4  21724  ablodivdiv4  21728  ablonnncan  21730  ablonnncan1  21732  ismndo1  21781  isrngod  21816  rngolz  21838  rngorz  21839  cnrngo  21840  vc0  21897  vcoprne  21907  isnvi  21941  nvmdi  21980  nvsubadd  21985  nvnpcan  21990  nvmeq0  21994  nvabs  22011  sspg  22076  ssps  22078  lno0  22106  nmoub3i  22123  nmblolbii  22149  ubthlem1  22221  minvecolem1  22225  elunop2  23365  pjclem4  23551  pj3si  23559  stlei  23592  csmdsymi  23686  atexch  23733  atcvatlem  23737  atcvat4i  23749  cdj3i  23793  iocinioc2  23979  elfzo1  23990  ofldsqr  24067  ofldchr  24071  unitdivcld  24104  rnlogblem  24196  esumpcvgval  24265  pwsiga  24310  prsiga  24311  sigainb  24316  insiga  24317  isrnmeas  24351  measres  24371  measdivcstOLD  24373  measdivcst  24374  imambfm  24407  dya2iocnrect  24426  ballotlemsup  24542  subfacp1lem1  24645  subfacp1lem2a  24646  iccllyscon  24717  cvmsi  24732  cvmlift2lem10  24779  relexpindlem  24919  fprodeq0  25079  poseq  25278  wfrlem15  25295  elno2  25333  brbtwn2  25559  colinearalg  25564  ax5seg  25592  axlowdim  25615  axcontlem2  25619  axcontlem4  25621  axcontlem9  25626  axcontlem10  25627  axcontlem12  25629  5segofs  25655  cgrextend  25657  segconeq  25659  segconeu  25660  trisegint  25677  fvtransport  25681  ifscgr  25693  cgrxfr  25704  btwnxfr  25705  lineext  25725  brofs2  25726  brifs2  25727  linecgr  25730  lineid  25732  btwnconn1lem4  25739  btwnconn1lem7  25742  btwnconn1lem8  25743  btwnconn1lem9  25744  btwnconn1lem11  25746  btwnconn1lem12  25747  btwnconn1lem13  25748  btwnconn1lem14  25749  btwnconn3  25752  brsegle2  25758  broutsideof2  25771  btwnoutside  25774  broutsideof3  25775  outsideoftr  25778  outsideofeu  25780  liness  25794  lineunray  25796  ellines  25801  supaddc  25948  supadd  25949  itg2addnclem2  25959  tailfb  26098  indexa  26127  seqpo  26143  nninfnub  26147  sstotbnd2  26175  rngohomsub  26281  crngm4  26305  igenval2  26368  prnc  26369  isfldidl  26370  ismrc  26447  jm2.17a  26717  congabseq  26731  jm2.18  26751  jm2.26a  26763  jm2.26lem3  26764  jm2.16nn0  26767  jm2.27c  26770  pmtrfrn  27070  pmtrfb  27076  psgnunilem2  27088  psgnunilem3  27089  deg1mhm  27196  pm13.194  27282  ubelsupr  27360  cncmpmax  27372  rfcnpre3  27373  rfcnpre4  27374  fmuldfeq  27382  fmul01lt1lem1  27383  fmul01lt1lem2  27384  climinf  27401  stoweidlem3  27421  stoweidlem14  27432  stoweidlem15  27433  stoweidlem20  27438  stoweidlem23  27441  stoweidlem26  27444  stoweidlem29  27447  stoweidlem34  27452  stoweidlem38  27456  stoweidlem39  27457  stoweidlem43  27461  stoweidlem44  27462  stoweidlem50  27468  stoweidlem51  27469  stoweidlem56  27474  stoweidlem59  27477  sigarcol  27523  sharhght  27524  cevathlem2  27527  cevath  27528  ndmaovdistr  27741  3vfriswmgra  27759  2pthfrgra  27765  3cyclfrgra  27769  frgranbnb  27774  vdn0frgrav2  27778  vdn1frgrav2  27780  vdgfrgragt2  27782  frgrancvvdeqlem3  27785  frgrancvvdeqlemC  27792  frgrancvvdeq  27795  frgrawopreglem5  27801  frgrawopreg  27802  bnj951  28485  bnj605  28617  bnj607  28626  bnj908  28641  bnj1001  28668  bnj1110  28690  bnj1128  28698  islshpcv  29169  isopiN  29297  latm12  29346  omllaw5N  29363  cmtcomlemN  29364  cmtbr3N  29370  omlfh3N  29375  atlen0  29426  cvlsupr2  29459  hlomcmat  29480  exatleN  29519  2llnneN  29524  cvrexchlem  29534  cvratlem  29536  atcvrj2b  29547  atltcvr  29550  atlelt  29553  atexchcvrN  29555  cvrat4  29558  2atjm  29560  atbtwnexOLDN  29562  atbtwnex  29563  4noncolr3  29568  3dimlem2  29574  3dimlem3  29576  3dimlem3OLDN  29577  3dimlem4  29579  3dimlem4OLDN  29580  3dim1  29582  3dim2  29583  3dim3  29584  1cvrat  29591  ps-2b  29597  3atlem4  29601  3atlem5  29602  3atlem6  29603  llnexatN  29636  llncvrlpln2  29672  2llnmj  29675  lplnexatN  29678  4atlem3a  29712  4atlem10  29721  4atlem11b  29723  4atlem11  29724  4atlem12b  29726  4atlem12  29727  lplncvrlvol2  29730  2lplnja  29734  2lplnj  29735  2lplnmj  29737  dalemswapyz  29771  dalemrot  29772  dalemswapyzps  29805  dalemrotps  29806  dalem51  29838  dalem52  29839  dath2  29852  lneq2at  29893  lncvrelatN  29896  cdlema1N  29906  cdlema2N  29907  cdlemblem  29908  paddval  29913  padd01  29926  padd02  29927  paddss12  29934  paddasslem2  29936  paddasslem4  29938  paddasslem6  29940  paddasslem9  29943  paddasslem10  29944  paddasslem12  29946  paddasslem15  29949  pmodlem1  29961  pmod2iN  29964  pmodN  29965  pmapjat1  29968  dalawlem1  29986  paddunN  30042  poml4N  30068  poml5N  30069  osumcllem6N  30076  pexmidlem6N  30090  pl42lem2N  30095  lhpexle1lem  30122  lhpexle1  30123  lhpexle2lem  30124  lhpexle3lem  30126  lhpmcvr5N  30142  lhpmcvr6N  30143  4atexlemswapqr  30178  4atexlemex6  30189  cdlemd2  30314  cdlemd5  30317  cdleme01N  30336  cdleme3b  30344  cdleme20i  30432  cdleme20m  30438  cdleme21d  30445  cdleme21e  30446  cdleme21i  30450  cdleme21j  30451  cdleme21  30452  cdleme22cN  30457  cdleme22f2  30462  cdleme24  30467  cdleme26f2ALTN  30479  cdleme26f2  30480  cdleme27a  30482  cdleme28a  30485  cdleme43fsv1snlem  30535  cdleme37m  30577  cdleme38m  30578  cdleme38n  30579  cdleme40n  30583  cdleme42mgN  30603  cdleme46f2g2  30608  cdleme46f2g1  30609  cdlemf1  30676  cdlemftr2  30681  cdlemg17pq  30787  cdlemg29  30820  cdlemg33b  30822  cdlemi  30935  tendocan  30939  cdlemk6  30952  cdlemk7  30963  cdlemk12  30965  cdlemk16  30972  cdlemk5u  30976  cdlemk18  30983  cdlemk19  30984  cdlemk7u  30985  cdlemk11u  30986  cdlemk12u  30987  cdlemk21N  30988  cdlemk20  30989  cdlemk7u-2N  31003  cdlemk11u-2N  31004  cdlemk12u-2N  31005  cdlemk21-2N  31006  cdlemk20-2N  31007  cdlemk22  31008  cdlemk31  31011  cdlemk23-3  31017  cdlemk24-3  31018  cdlemk25-3  31019  cdlemk26b-3  31020  cdlemk26-3  31021  cdlemk27-3  31022  cdlemk28-3  31023  cdlemk33N  31024  cdlemk34  31025  cdlemky  31041  cdlemk11ta  31044  cdlemk19ylem  31045  cdlemk35s-id  31053  cdlemk39s-id  31055  cdlemk19xlem  31057  cdlemk11tc  31060  cdlemk11t  31061  cdlemk47  31064  cdlemk53b  31071  cdlemk53  31072  cdlemkyyN  31077  cdlemk55u1  31080  cdlemk19u1  31084  erng1r  31110  dvalveclem  31141  diclspsn  31310  dihmeetlem20N  31442  islpoldN  31600  lpolconN  31603
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator