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

Theorem 3jca 1132
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 520 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  /\  th )
)
5 df-3an 936 . 2  |-  ( ( ps  /\  ch  /\  th )  <->  ( ( ps 
/\  ch )  /\  th ) )
64, 5sylibr 203 1  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    /\ w3a 934
This theorem is referenced by:  3jcad  1133  mpbir3and  1135  syl3anbrc  1136  3anim123i  1137  syl3anc  1182  syl13anc  1184  syl31anc  1185  syl113anc  1194  syl131anc  1195  syl311anc  1196  syl33anc  1197  syl133anc  1205  syl313anc  1206  syl331anc  1207  syl333anc  1214  3jaob  1244  mp3and  1280  soltmin  5082  tz7.49  6457  oeeulem  6599  domss2  7020  intrnfi  7170  dffi2  7176  elfiun  7183  hartogslem1  7257  wemaplem2  7262  oemapvali  7386  cfss  7891  cofsmo  7895  axdc3lem4  8079  axdc4lem  8081  fpwwe2lem6  8257  fpwwe2lem13  8264  canth4  8269  intwun  8357  r1limwun  8358  wunex2  8360  tskwun  8406  gruwun  8435  intgru  8436  wfgru  8438  grutsk1  8443  le2tri3i  8949  ledivmulOLD  9630  supmul1  9719  supmullem2  9721  eluzp1p1  10253  peano2uz  10272  rpnnen1lem5  10346  ixxun  10672  elioc2  10713  elico2  10714  elicc2  10715  iccsupr  10736  iccsplit  10768  fzrev3  10849  fseq1p1m1  10857  elfzo2  10878  elfzo0  10904  intfrac2  10962  intfracq  10963  seqf1olem2  11086  remullem  11613  sqr0lem  11726  sqrlem3  11730  resqreu  11738  resqrcl  11739  sqrneglem  11752  sqreulem  11843  eqsqrd  11851  climsup  12143  fsumcvg3  12202  supcvg  12314  mertenslem2  12341  sin02gt0  12472  ruclem1  12509  ruclem2  12510  ruclem11  12518  gcdcllem3  12692  rppwr  12736  qredeq  12785  maxprmfct  12792  pythagtriplem6  12874  pythagtriplem7  12875  pythagtriplem19  12886  pclem  12891  prmreclem1  12963  ramcl  13076  iscatd2  13583  issubc3  13723  prsref  14066  posref  14085  isposd  14089  isposi  14090  latjlej1  14171  latmlem1  14187  latledi  14195  latj32  14203  mod2ile  14212  lubss  14225  pslem  14315  letsr  14349  0mhm  14435  resmhm  14436  resmhm2  14437  resmhm2b  14438  mhmco  14439  prdspjmhm  14443  pwsdiagmhm  14445  pwsco1mhm  14446  pwsco2mhm  14447  frmdup1  14486  grpinvid1  14530  grpinvid2  14531  grplcan  14534  issubg2  14636  issubg4  14638  ghmmhm  14693  cayley  14789  lsmelvali  14961  pj1id  15008  frgpmhm  15074  mulgmhm  15127  dmdprdsplit  15282  ablfac1lem  15303  ablfac2  15324  rnglz  15377  rngrz  15378  isrhm2d  15506  subrgunit  15563  issubrg2  15565  islmodd  15633  islmhm2  15795  islmhmd  15796  reslmhm  15809  islbs2  15907  islbs3  15908  isassad  16063  isphld  16558  iscldtop  16832  iscnp2  16969  cnpnei  16993  cnpco  16996  hausnei2  17081  nconsubb  17149  nlly2i  17202  elptr  17268  upxp  17317  elmptrab2  17523  opnfbas  17537  isfil2  17551  isfild  17553  infil  17558  fsubbas  17562  neifil  17575  fbasrn  17579  rnelfmlem  17647  fmfnfmlem4  17652  fmfnfm  17653  flimclslem  17679  flimsncls  17681  istgp2  17774  tsmsfbas  17810  tmslem  18028  stdbdmopn  18064  isngp4  18133  sranlm  18195  nlmtlm  18204  lssnlm  18211  nmoleub  18240  qdensere  18279  iirev  18427  iihalf1  18429  iihalf2  18431  iimulcl  18435  icoopnst  18437  iocopnst  18438  evth  18457  pcoptcl  18519  pcorevcl  18523  nmhmcn  18601  cphsubrglem  18613  tchcph  18667  cmetcaulem  18714  hlprlem  18784  minveclem1  18788  minveclem3b  18792  ivthlem2  18812  ivthlem3  18813  vitalilem2  18964  mbfsup  19019  i1fd  19036  itg2seq  19097  itg2mono  19108  itgsplitioo  19192  dvfsumlem4  19376  dvfsumrlim3  19380  evlslem1  19399  mdegaddle  19460  mdegmullem  19464  ply1divmo  19521  ply1remlem  19548  fta1b  19555  plyremlem  19684  aannenlem2  19709  aalioulem5  19716  aalioulem6  19717  aaliou  19718  aaliou3lem3  19724  psercnlem2  19800  psercnlem1  19801  pserdvlem1  19803  ptolemy  19864  quart1cl  20150  quartlem2  20154  quartlem3  20155  quartlem4  20156  jensenlem2  20282  emcllem7  20295  ftalem4  20313  basellem2  20319  perfectlem1  20468  dchrelbasd  20478  dchrmulcl  20488  dchrinv  20500  lgsdchr  20587  pntlemd  20743  pntlemc  20744  pntlemb  20746  pntlemg  20747  grpoidinvlem2  20872  grpoidval  20883  grpoidinv2  20885  grpoinv  20894  grpoinvid1  20897  grpoinvid2  20898  grpolcan  20900  grpo2inv  20906  grpomuldivass  20916  grponpncan  20922  ablo4  20954  ablodivdiv4  20958  ablonnncan  20960  ablonnncan1  20962  ismndo1  21011  isrngod  21046  rngolz  21068  rngorz  21069  cnrngo  21070  vc0  21125  vcoprne  21135  isnvi  21169  nvmdi  21208  nvsubadd  21213  nvnpcan  21218  nvmeq0  21222  nvabs  21239  sspg  21304  ssps  21306  lno0  21334  nmoub3i  21351  nmblolbii  21377  ubthlem1  21449  minvecolem1  21453  elunop2  22593  pjclem4  22779  pj3si  22787  stlei  22820  csmdsymi  22914  atexch  22961  atcvatlem  22965  atcvat4i  22977  cdj3i  23021  bcm1n  23032  ballotlemsup  23063  ballotlemsdom  23070  lt2addrd  23249  xlt2addrd  23253  eliccelico  23270  elicoelioo  23271  iocinioc2  23272  elfzo1  23279  unitdivcld  23285  cnre2csqlem  23294  tpr2rico  23296  disjabrex  23359  disjabrexf  23360  rnlogblem  23401  rnlogbval  23402  nnlogbexp  23406  esumpcvgval  23446  pwsiga  23491  prsiga  23492  sigainb  23497  insiga  23498  isrnmeas  23531  measres  23549  measdivcstOLD  23551  measdivcst  23552  cntmeas  23553  imambfm  23567  dya2iocseg  23579  probdsb  23625  dstrvprob  23672  subfacp1lem1  23710  subfacp1lem2a  23711  iccllyscon  23781  cvmsi  23796  cvmlift2lem10  23843  vdgr0  23892  relexpindlem  24036  poseq  24253  wfrlem15  24270  elno2  24308  brbtwn2  24533  colinearalg  24538  ax5seg  24566  axlowdim  24589  axcontlem2  24593  axcontlem4  24595  axcontlem9  24600  axcontlem10  24601  axcontlem12  24603  5segofs  24629  cgrextend  24631  segconeq  24633  segconeu  24634  trisegint  24651  fvtransport  24655  ifscgr  24667  cgrxfr  24678  btwnxfr  24679  lineext  24699  brofs2  24700  brifs2  24701  linecgr  24704  lineid  24706  btwnconn1lem4  24713  btwnconn1lem7  24716  btwnconn1lem8  24717  btwnconn1lem9  24718  btwnconn1lem11  24720  btwnconn1lem12  24721  btwnconn1lem13  24722  btwnconn1lem14  24723  btwnconn3  24726  brsegle2  24732  broutsideof2  24745  btwnoutside  24748  broutsideof3  24749  outsideoftr  24752  outsideofeu  24754  liness  24768  lineunray  24770  ellines  24775  iccss3  25134  cljo  25186  clme  25187  int2pre  25237  definc  25279  dfps2  25289  reacomsmgrp1  25343  reacomsmgrp3  25345  reacomsmgrp4  25346  resgcom  25351  grpodrcan  25375  grpodlcan  25376  rltrran  25414  rltrooo  25415  dblsubvec  25474  mvecrtol2  25477  glmrngo  25482  svli2  25484  vri  25492  truni1  25505  cbci  25508  mslb1  25607  trnij  25615  xrletr2  25618  flfnein  25621  lvsovso  25626  lvsovso3  25628  addcanri  25666  distmlva  25688  distsava  25689  icccon2  25700  icccon4  25702  dualalg  25782  dualded  25783  homgrf  25802  imonclem  25813  ismonc  25814  idmon  25817  immon  25818  iepiclem  25823  isepic  25824  idfisf  25841  idsubfun  25858  tartarmap  25888  fnctartar  25907  fnctartar2  25908  setiscat  25979  bisig0  26062  isconcl6a  26103  isside  26166  bosser  26167  pdiveql  26168  tailfb  26326  indexa  26412  seqpo  26457  nninfnub  26461  sstotbnd2  26498  rngohomsub  26604  crngm4  26628  igenval2  26691  prnc  26692  isfldidl  26693  ismrc  26776  jm2.17a  27047  congabseq  27061  jm2.18  27081  jm2.26a  27093  jm2.26lem3  27094  jm2.16nn0  27097  jm2.27c  27100  pmtrfrn  27400  pmtrfb  27406  psgnunilem2  27418  psgnunilem3  27419  deg1mhm  27526  pm13.194  27612  ubelsupr  27691  fcnre  27696  fnchoice  27700  refsumcn  27701  cncmpmax  27703  rfcnpre3  27704  rfcnpre4  27705  refsum2cnlem1  27708  fmul01  27710  fmulcl  27711  fmuldfeq  27713  fmul01lt1lem1  27714  fmul01lt1lem2  27715  climinf  27732  climsuselem1  27733  climsuse  27734  ibliccsinexp  27745  itgsinexplem1  27748  itgsinexp  27749  stoweidlem1  27750  stoweidlem3  27752  stoweidlem5  27754  stoweidlem7  27756  stoweidlem10  27759  stoweidlem11  27760  stoweidlem13  27762  stoweidlem14  27763  stoweidlem15  27764  stoweidlem16  27765  stoweidlem17  27766  stoweidlem18  27767  stoweidlem19  27768  stoweidlem20  27769  stoweidlem21  27770  stoweidlem22  27771  stoweidlem23  27772  stoweidlem24  27773  stoweidlem25  27774  stoweidlem26  27775  stoweidlem28  27777  stoweidlem29  27778  stoweidlem31  27780  stoweidlem32  27781  stoweidlem34  27783  stoweidlem36  27785  stoweidlem37  27786  stoweidlem38  27787  stoweidlem39  27788  stoweidlem40  27789  stoweidlem41  27790  stoweidlem42  27791  stoweidlem43  27792  stoweidlem44  27793  stoweidlem45  27794  stoweidlem46  27795  stoweidlem47  27796  stoweidlem48  27797  stoweidlem49  27798  stoweidlem50  27799  stoweidlem51  27800  stoweidlem52  27801  stoweidlem53  27802  stoweidlem54  27803  stoweidlem55  27804  stoweidlem56  27805  stoweidlem57  27806  stoweidlem58  27807  stoweidlem59  27808  stoweidlem60  27809  stoweidlem61  27810  stoweidlem62  27811  stoweid  27812  wallispilem1  27814  wallispilem3  27816  wallispilem4  27817  wallispilem5  27818  wallispi  27819  wallispi2lem1  27820  wallispi2  27822  stirlinglem3  27825  stirlinglem5  27827  stirlinglem6  27828  stirlinglem10  27832  sigarcol  27854  sharhght  27855  cevathlem2  27858  cevath  27859  ndmaovdistr  28067  3vfriswmgra  28183  bnj951  28807  bnj605  28939  bnj607  28948  bnj908  28963  bnj1001  28990  bnj1110  29012  bnj1128  29020  islshpcv  29243  isopiN  29371  latm12  29420  omllaw5N  29437  cmtcomlemN  29438  cmtbr3N  29444  omlfh3N  29449  atlen0  29500  cvlsupr2  29533  hlomcmat  29554  exatleN  29593  2llnneN  29598  cvrexchlem  29608  cvratlem  29610  atcvrj2b  29621  atltcvr  29624  atlelt  29627  atexchcvrN  29629  cvrat4  29632  2atjm  29634  atbtwnexOLDN  29636  atbtwnex  29637  4noncolr3  29642  3dimlem2  29648  3dimlem3  29650  3dimlem3OLDN  29651  3dimlem4  29653  3dimlem4OLDN  29654  3dim1  29656  3dim2  29657  3dim3  29658  1cvrat  29665  ps-2b  29671  3atlem4  29675  3atlem5  29676  3atlem6  29677  llnexatN  29710  llncvrlpln2  29746  2llnmj  29749  lplnexatN  29752  4atlem3a  29786  4atlem10  29795  4atlem11b  29797  4atlem11  29798  4atlem12b  29800  4atlem12  29801  lplncvrlvol2  29804  2lplnja  29808  2lplnj  29809  2lplnmj  29811  dalemswapyz  29845  dalemrot  29846  dalemswapyzps  29879  dalemrotps  29880  dalem51  29912  dalem52  29913  dath2  29926  lneq2at  29967  lncvrelatN  29970  cdlema1N  29980  cdlema2N  29981  cdlemblem  29982  paddval  29987  padd01  30000  padd02  30001  paddss12  30008  paddasslem2  30010  paddasslem4  30012  paddasslem6  30014  paddasslem9  30017  paddasslem10  30018  paddasslem12  30020  paddasslem15  30023  pmodlem1  30035  pmod2iN  30038  pmodN  30039  pmapjat1  30042  dalawlem1  30060  paddunN  30116  poml4N  30142  poml5N  30143  osumcllem6N  30150  pexmidlem6N  30164  pl42lem2N  30169  lhpexle1lem  30196  lhpexle1  30197  lhpexle2lem  30198  lhpexle3lem  30200  lhpmcvr5N  30216  lhpmcvr6N  30217  4atexlemswapqr  30252  4atexlemex6  30263  cdlemd2  30388  cdlemd5  30391  cdleme01N  30410  cdleme3b  30418  cdleme20i  30506  cdleme20m  30512  cdleme21d  30519  cdleme21e  30520  cdleme21i  30524  cdleme21j  30525  cdleme21  30526  cdleme22cN  30531  cdleme22f2  30536  cdleme24  30541  cdleme26f2ALTN  30553  cdleme26f2  30554  cdleme27a  30556  cdleme28a  30559  cdleme43fsv1snlem  30609  cdleme37m  30651  cdleme38m  30652  cdleme38n  30653  cdleme40n  30657  cdleme42mgN  30677  cdleme46f2g2  30682  cdleme46f2g1  30683  cdlemf1  30750  cdlemftr2  30755  cdlemg17pq  30861  cdlemg29  30894  cdlemg33b  30896  cdlemi  31009  tendocan  31013  cdlemk6  31026  cdlemk7  31037  cdlemk12  31039  cdlemk16  31046  cdlemk5u  31050  cdlemk18  31057  cdlemk19  31058  cdlemk7u  31059  cdlemk11u  31060  cdlemk12u  31061  cdlemk21N  31062  cdlemk20  31063  cdlemk7u-2N  31077  cdlemk11u-2N  31078  cdlemk12u-2N  31079  cdlemk21-2N  31080  cdlemk20-2N  31081  cdlemk22  31082  cdlemk31  31085  cdlemk23-3  31091  cdlemk24-3  31092  cdlemk25-3  31093  cdlemk26b-3  31094  cdlemk26-3  31095  cdlemk27-3  31096  cdlemk28-3  31097  cdlemk33N  31098  cdlemk34  31099  cdlemky  31115  cdlemk11ta  31118  cdlemk19ylem  31119  cdlemk35s-id  31127  cdlemk39s-id  31129  cdlemk19xlem  31131  cdlemk11tc  31134  cdlemk11t  31135  cdlemk47  31138  cdlemk53b  31145  cdlemk53  31146  cdlemkyyN  31151  cdlemk55u1  31154  cdlemk19u1  31158  erng1r  31184  dvalveclem  31215  diclspsn  31384  dihmeetlem20N  31516  islpoldN  31674  lpolconN  31677
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 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator