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  5232  tz7.49  6661  oeeulem  6803  domss2  7225  intrnfi  7379  dffi2  7386  elfiun  7393  hartogslem1  7467  wemaplem2  7472  oemapvali  7596  cfss  8101  cofsmo  8105  axdc3lem4  8289  axdc4lem  8291  fpwwe2lem6  8466  fpwwe2lem13  8473  canth4  8478  intwun  8566  r1limwun  8567  wunex2  8569  tskwun  8615  gruwun  8644  intgru  8645  wfgru  8647  grutsk1  8652  le2tri3i  9159  ledivmulOLD  9840  supmul1  9929  supmullem2  9931  eluzp1p1  10467  peano2uz  10486  rpnnen1lem5  10560  ixxun  10888  elioc2  10929  elico2  10930  elicc2  10931  iccsupr  10953  iccsplit  10985  fzrev3  11067  fseq1p1m1  11077  elfzo2  11098  elfzo0  11126  elfzo1  11128  elfznelfzo  11147  intfrac2  11194  intfracq  11195  seqf1olem2  11318  hashprb  11623  brfi1uzind  11670  remullem  11888  sqr0lem  12001  sqrlem3  12005  resqreu  12013  resqrcl  12014  sqrneglem  12027  sqreulem  12118  eqsqrd  12126  climsup  12418  fsumcvg3  12478  supcvg  12590  mertenslem2  12617  sin02gt0  12748  ruclem1  12785  ruclem2  12786  ruclem11  12794  gcdcllem3  12968  rppwr  13012  qredeq  13061  maxprmfct  13068  pythagtriplem6  13150  pythagtriplem7  13151  pythagtriplem19  13162  pclem  13167  prmreclem1  13239  ramcl  13352  iscatd2  13861  issubc3  14001  prsref  14344  posref  14363  isposd  14367  isposi  14368  latjlej1  14449  latmlem1  14465  latledi  14473  latj32  14481  mod2ile  14490  lubss  14503  pslem  14593  letsr  14627  0mhm  14713  resmhm  14714  resmhm2  14715  resmhm2b  14716  mhmco  14717  prdspjmhm  14721  pwsdiagmhm  14723  pwsco1mhm  14724  pwsco2mhm  14725  frmdup1  14764  grpinvid1  14808  grpinvid2  14809  grplcan  14812  issubg2  14914  issubg4  14916  ghmmhm  14971  cayley  15067  lsmelvali  15239  pj1id  15286  frgpmhm  15352  mulgmhm  15405  dmdprdsplit  15560  ablfac1lem  15581  ablfac2  15602  rnglz  15655  rngrz  15656  isrhm2d  15784  subrgunit  15841  issubrg2  15843  islmodd  15911  islmhm2  16069  islmhmd  16070  reslmhm  16083  islbs2  16181  islbs3  16182  isassad  16337  isphld  16840  iscldtop  17114  neiptoptop  17150  iscnp2  17257  cnpnei  17282  cnpco  17285  hausnei2  17371  nconsubb  17439  nlly2i  17492  elptr  17558  upxp  17608  elmptrab2  17813  opnfbas  17827  isfil2  17841  isfild  17843  infil  17848  fsubbas  17852  neifil  17865  fbasrn  17869  rnelfmlem  17937  fmfnfmlem4  17942  fmfnfm  17943  flimclslem  17969  flimsncls  17971  istgp2  18074  tsmsfbas  18110  ustfilxp  18195  trust  18212  ustuqtop4  18227  tuslem  18250  tmslem  18465  stdbdmopn  18501  metustexhalfOLD  18546  metustexhalf  18547  metustfbasOLD  18548  metustfbas  18549  metustOLD  18550  metust  18551  isngp4  18611  sranlm  18673  nlmtlm  18682  lssnlm  18689  nmoleub  18718  qdensere  18757  iirev  18907  iihalf1  18909  iihalf2  18911  iimulcl  18915  icoopnst  18917  iocopnst  18918  evth  18937  pcoptcl  18999  pcorevcl  19003  nmhmcn  19081  cphsubrglem  19093  tchcph  19147  cmetcaulem  19194  hlprlem  19274  minveclem1  19278  minveclem3b  19282  ivthlem2  19302  ivthlem3  19303  vitalilem2  19454  mbfsup  19509  i1fd  19526  itg2seq  19587  itg2mono  19598  itgsplitioo  19682  dvfsumlem4  19866  dvfsumrlim3  19870  evlslem1  19889  mdegaddle  19950  mdegmullem  19954  ply1divmo  20011  ply1remlem  20038  fta1b  20045  plyremlem  20174  aannenlem2  20199  aalioulem5  20206  aalioulem6  20207  aaliou  20208  aaliou3lem3  20214  psercnlem2  20293  psercnlem1  20294  pserdvlem1  20296  ptolemy  20357  quart1cl  20647  quartlem2  20651  quartlem3  20652  quartlem4  20653  jensenlem2  20779  emcllem7  20793  ftalem4  20811  basellem2  20817  perfectlem1  20966  dchrelbasd  20976  dchrmulcl  20986  dchrinv  20998  lgsdchr  21085  pntlemd  21241  pntlemc  21242  pntlemb  21244  pntlemg  21245  usgra2edg  21355  wlkbprop  21487  wlkonwlk  21488  spthispth  21526  pthdepisspth  21527  isspthonpth  21537  1pthon  21544  constr2trl  21552  2pthon  21555  wlkdvspthlem  21560  wlkdvspth  21561  cyclispthon  21573  fargshiftf1  21577  constr3lem4  21587  constr3lem5  21588  constr3trllem1  21590  constr3trllem2  21591  constr3trl  21599  constr3pth  21600  constr3cyclp  21602  4cycl4dv  21607  vdgr0  21624  vdusgraval  21631  vdgrnn0pnf  21633  eupatrl  21643  grpoidinvlem2  21746  grpoidval  21757  grpoidinv2  21759  grpoinv  21768  grpoinvid1  21771  grpoinvid2  21772  grpolcan  21774  grpo2inv  21780  grpomuldivass  21790  grponpncan  21796  ablo4  21828  ablodivdiv4  21832  ablonnncan  21834  ablonnncan1  21836  ismndo1  21885  isrngod  21920  rngolz  21942  rngorz  21943  cnrngo  21944  vc0  22001  vcoprne  22011  isnvi  22045  nvmdi  22084  nvsubadd  22089  nvnpcan  22094  nvmeq0  22098  nvabs  22115  sspg  22180  ssps  22182  lno0  22210  nmoub3i  22227  nmblolbii  22253  ubthlem1  22325  minvecolem1  22329  elunop2  23469  pjclem4  23655  pj3si  23663  stlei  23696  csmdsymi  23790  atexch  23837  atcvatlem  23841  atcvat4i  23853  cdj3i  23897  iocinioc2  24095  xrstos  24154  ofldsqr  24193  ofldchr  24197  unitdivcld  24252  rnlogblem  24352  esumpcvgval  24421  pwsiga  24466  prsiga  24467  sigainb  24472  insiga  24473  isrnmeas  24507  measres  24529  measdivcstOLD  24531  measdivcst  24532  imambfm  24565  dya2iocnrect  24584  sibf0  24602  sibfof  24607  ballotlemsup  24715  subfacp1lem1  24818  subfacp1lem2a  24819  iccllyscon  24890  cvmsi  24905  cvmlift2lem10  24952  relexpindlem  25092  fprodeq0  25252  poseq  25467  wfrlem15  25484  elno2  25522  brbtwn2  25748  colinearalg  25753  ax5seg  25781  axlowdim  25804  axcontlem2  25808  axcontlem4  25810  axcontlem9  25815  axcontlem10  25816  axcontlem12  25818  5segofs  25844  cgrextend  25846  segconeq  25848  segconeu  25849  trisegint  25866  fvtransport  25870  ifscgr  25882  cgrxfr  25893  btwnxfr  25894  lineext  25914  brofs2  25915  brifs2  25916  linecgr  25919  lineid  25921  btwnconn1lem4  25928  btwnconn1lem7  25931  btwnconn1lem8  25932  btwnconn1lem9  25933  btwnconn1lem11  25935  btwnconn1lem12  25936  btwnconn1lem13  25937  btwnconn1lem14  25938  btwnconn3  25941  brsegle2  25947  broutsideof2  25960  btwnoutside  25963  broutsideof3  25964  outsideoftr  25967  outsideofeu  25969  liness  25983  lineunray  25985  ellines  25990  supaddc  26137  supadd  26138  mblfinlem2  26144  ismblfin  26146  itg2addnclem2  26156  tailfb  26296  indexa  26325  seqpo  26341  nninfnub  26345  sstotbnd2  26373  rngohomsub  26479  crngm4  26503  igenval2  26566  prnc  26567  isfldidl  26568  ismrc  26645  jm2.17a  26915  congabseq  26929  jm2.18  26949  jm2.26a  26961  jm2.26lem3  26962  jm2.16nn0  26965  jm2.27c  26968  pmtrfrn  27268  pmtrfb  27274  psgnunilem2  27286  psgnunilem3  27287  deg1mhm  27394  pm13.194  27480  ubelsupr  27558  cncmpmax  27570  rfcnpre3  27571  rfcnpre4  27572  fmuldfeq  27580  fmul01lt1lem1  27581  fmul01lt1lem2  27582  climinf  27599  stoweidlem3  27619  stoweidlem14  27630  stoweidlem15  27631  stoweidlem20  27636  stoweidlem23  27639  stoweidlem26  27642  stoweidlem29  27645  stoweidlem34  27650  stoweidlem38  27654  stoweidlem39  27655  stoweidlem43  27659  stoweidlem44  27660  stoweidlem50  27666  stoweidlem51  27667  stoweidlem56  27672  stoweidlem59  27675  sigarcol  27721  sharhght  27722  cevathlem2  27725  cevath  27726  ndmaovdistr  27938  el2xptp0  27949  oteqimp  27951  elfzmlbm  27977  elfzmlbp  27978  elfzelfzelfz  27981  ubmelfzo  27986  ubmelm1fzo  27987  fzo1fzo0n0  27988  swrd0  28002  swrd0swrd  28009  swrdswrdlem  28010  swrd0swrdid  28012  swrdswrd0  28013  swrdccatin1  28016  swrdccatin2  28018  swrdccatin12lem1  28019  swrdccatin12lem3a  28021  swrdccatin12lem3b  28022  swrdccatin12lem3c  28023  swrdccatin12lem3  28024  swrdccatin12lem4  28025  swrdccatin12  28026  swrdccatin12b  28027  swrdccatin12c  28028  swrdccat3  28029  swrdccat3b  28031  usgra2pthspth  28035  usgra2wlkspth  28038  usgra2pthlem1  28040  usgra2pth  28041  usgra2adedgspth  28045  usgra2adedgwlk  28046  usgra2adedgwlkon  28047  el2wlkonot  28066  el2spthonot  28067  el2spthonot0  28068  el2wlkonotot0  28069  2wlkonot3v  28072  2spthonot3v  28073  usg2wotspth  28081  usg2spthonot0  28086  usg2spthonot1  28087  usgfidegfi  28090  3vfriswmgra  28109  2pthfrgra  28115  3cyclfrgra  28119  frgranbnb  28124  vdn0frgrav2  28128  vdn1frgrav2  28130  vdgfrgragt2  28132  frgrancvvdeqlem3  28135  frgrancvvdeqlemC  28142  frgrancvvdeq  28145  frgrawopreglem5  28151  frgrawopreg  28152  frg2woteu  28158  frg2woteqm  28162  frg2woteq  28163  usg2spot2nb  28168  usgreg2spot  28170  bnj951  28852  bnj605  28984  bnj607  28993  bnj908  29008  bnj1001  29035  bnj1110  29057  bnj1128  29065  islshpcv  29536  isopiN  29664  latm12  29713  omllaw5N  29730  cmtcomlemN  29731  cmtbr3N  29737  omlfh3N  29742  atlen0  29793  cvlsupr2  29826  hlomcmat  29847  exatleN  29886  2llnneN  29891  cvrexchlem  29901  cvratlem  29903  atcvrj2b  29914  atltcvr  29917  atlelt  29920  atexchcvrN  29922  cvrat4  29925  2atjm  29927  atbtwnexOLDN  29929  atbtwnex  29930  4noncolr3  29935  3dimlem2  29941  3dimlem3  29943  3dimlem3OLDN  29944  3dimlem4  29946  3dimlem4OLDN  29947  3dim1  29949  3dim2  29950  3dim3  29951  1cvrat  29958  ps-2b  29964  3atlem4  29968  3atlem5  29969  3atlem6  29970  llnexatN  30003  llncvrlpln2  30039  2llnmj  30042  lplnexatN  30045  4atlem3a  30079  4atlem10  30088  4atlem11b  30090  4atlem11  30091  4atlem12b  30093  4atlem12  30094  lplncvrlvol2  30097  2lplnja  30101  2lplnj  30102  2lplnmj  30104  dalemswapyz  30138  dalemrot  30139  dalemswapyzps  30172  dalemrotps  30173  dalem51  30205  dalem52  30206  dath2  30219  lneq2at  30260  lncvrelatN  30263  cdlema1N  30273  cdlema2N  30274  cdlemblem  30275  paddval  30280  padd01  30293  padd02  30294  paddss12  30301  paddasslem2  30303  paddasslem4  30305  paddasslem6  30307  paddasslem9  30310  paddasslem10  30311  paddasslem12  30313  paddasslem15  30316  pmodlem1  30328  pmod2iN  30331  pmodN  30332  pmapjat1  30335  dalawlem1  30353  paddunN  30409  poml4N  30435  poml5N  30436  osumcllem6N  30443  pexmidlem6N  30457  pl42lem2N  30462  lhpexle1lem  30489  lhpexle1  30490  lhpexle2lem  30491  lhpexle3lem  30493  lhpmcvr5N  30509  lhpmcvr6N  30510  4atexlemswapqr  30545  4atexlemex6  30556  cdlemd2  30681  cdlemd5  30684  cdleme01N  30703  cdleme3b  30711  cdleme20i  30799  cdleme20m  30805  cdleme21d  30812  cdleme21e  30813  cdleme21i  30817  cdleme21j  30818  cdleme21  30819  cdleme22cN  30824  cdleme22f2  30829  cdleme24  30834  cdleme26f2ALTN  30846  cdleme26f2  30847  cdleme27a  30849  cdleme28a  30852  cdleme43fsv1snlem  30902  cdleme37m  30944  cdleme38m  30945  cdleme38n  30946  cdleme40n  30950  cdleme42mgN  30970  cdleme46f2g2  30975  cdleme46f2g1  30976  cdlemf1  31043  cdlemftr2  31048  cdlemg17pq  31154  cdlemg29  31187  cdlemg33b  31189  cdlemi  31302  tendocan  31306  cdlemk6  31319  cdlemk7  31330  cdlemk12  31332  cdlemk16  31339  cdlemk5u  31343  cdlemk18  31350  cdlemk19  31351  cdlemk7u  31352  cdlemk11u  31353  cdlemk12u  31354  cdlemk21N  31355  cdlemk20  31356  cdlemk7u-2N  31370  cdlemk11u-2N  31371  cdlemk12u-2N  31372  cdlemk21-2N  31373  cdlemk20-2N  31374  cdlemk22  31375  cdlemk31  31378  cdlemk23-3  31384  cdlemk24-3  31385  cdlemk25-3  31386  cdlemk26b-3  31387  cdlemk26-3  31388  cdlemk27-3  31389  cdlemk28-3  31390  cdlemk33N  31391  cdlemk34  31392  cdlemky  31408  cdlemk11ta  31411  cdlemk19ylem  31412  cdlemk35s-id  31420  cdlemk39s-id  31422  cdlemk19xlem  31424  cdlemk11tc  31427  cdlemk11t  31428  cdlemk47  31431  cdlemk53b  31438  cdlemk53  31439  cdlemkyyN  31444  cdlemk55u1  31447  cdlemk19u1  31451  erng1r  31477  dvalveclem  31508  diclspsn  31677  dihmeetlem20N  31809  islpoldN  31967  lpolconN  31970
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