MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3jca Structured version   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  5265  tz7.49  6694  oeeulem  6836  domss2  7258  intrnfi  7413  dffi2  7420  elfiun  7427  hartogslem1  7503  wemaplem2  7508  oemapvali  7632  cfss  8137  cofsmo  8141  axdc3lem4  8325  axdc4lem  8327  fpwwe2lem6  8502  fpwwe2lem13  8509  canth4  8514  intwun  8602  r1limwun  8603  wunex2  8605  tskwun  8651  gruwun  8680  intgru  8681  wfgru  8683  grutsk1  8688  le2tri3i  9195  ledivmulOLD  9876  supmul1  9965  supmullem2  9967  eluzp1p1  10503  peano2uz  10522  rpnnen1lem5  10596  ixxun  10924  elioc2  10965  elico2  10966  elicc2  10967  iccsupr  10989  iccsplit  11021  fzrev3  11103  fseq1p1m1  11114  elfzo2  11135  elfzo0  11163  elfzo1  11165  elfznelfzo  11184  intfrac2  11231  intfracq  11232  seqf1olem2  11355  hashprb  11660  brfi1uzind  11707  remullem  11925  sqr0lem  12038  sqrlem3  12042  resqreu  12050  resqrcl  12051  sqrneglem  12064  sqreulem  12155  eqsqrd  12163  climsup  12455  fsumcvg3  12515  supcvg  12627  mertenslem2  12654  sin02gt0  12785  ruclem1  12822  ruclem2  12823  ruclem11  12831  gcdcllem3  13005  rppwr  13049  qredeq  13098  maxprmfct  13105  pythagtriplem6  13187  pythagtriplem7  13188  pythagtriplem19  13199  pclem  13204  prmreclem1  13276  ramcl  13389  iscatd2  13898  issubc3  14038  prsref  14381  posref  14400  isposd  14404  isposi  14405  latjlej1  14486  latmlem1  14502  latledi  14510  latj32  14518  mod2ile  14527  lubss  14540  pslem  14630  letsr  14664  0mhm  14750  resmhm  14751  resmhm2  14752  resmhm2b  14753  mhmco  14754  prdspjmhm  14758  pwsdiagmhm  14760  pwsco1mhm  14761  pwsco2mhm  14762  frmdup1  14801  grpinvid1  14845  grpinvid2  14846  grplcan  14849  issubg2  14951  issubg4  14953  ghmmhm  15008  cayley  15104  lsmelvali  15276  pj1id  15323  frgpmhm  15389  mulgmhm  15442  dmdprdsplit  15597  ablfac1lem  15618  ablfac2  15639  rnglz  15692  rngrz  15693  isrhm2d  15821  subrgunit  15878  issubrg2  15880  islmodd  15948  islmhm2  16106  islmhmd  16107  reslmhm  16120  islbs2  16218  islbs3  16219  isassad  16374  isphld  16877  iscldtop  17151  neiptoptop  17187  iscnp2  17295  cnpnei  17320  cnpco  17323  hausnei2  17409  nconsubb  17478  nlly2i  17531  elptr  17597  upxp  17647  elmptrab2  17852  opnfbas  17866  isfil2  17880  isfild  17882  infil  17887  fsubbas  17891  neifil  17904  fbasrn  17908  rnelfmlem  17976  fmfnfmlem4  17981  fmfnfm  17982  flimclslem  18008  flimsncls  18010  istgp2  18113  tsmsfbas  18149  ustfilxp  18234  trust  18251  ustuqtop4  18266  tuslem  18289  tmslem  18504  stdbdmopn  18540  metustexhalfOLD  18585  metustexhalf  18586  metustfbasOLD  18587  metustfbas  18588  metustOLD  18589  metust  18590  isngp4  18650  sranlm  18712  nlmtlm  18721  lssnlm  18728  nmoleub  18757  qdensere  18796  iirev  18946  iihalf1  18948  iihalf2  18950  iimulcl  18954  icoopnst  18956  iocopnst  18957  evth  18976  pcoptcl  19038  pcorevcl  19042  nmhmcn  19120  cphsubrglem  19132  tchcph  19186  cmetcaulem  19233  hlprlem  19313  minveclem1  19317  minveclem3b  19321  ivthlem2  19341  ivthlem3  19342  vitalilem2  19493  mbfsup  19548  i1fd  19565  itg2seq  19626  itg2mono  19637  itgsplitioo  19721  dvfsumlem4  19905  dvfsumrlim3  19909  evlslem1  19928  mdegaddle  19989  mdegmullem  19993  ply1divmo  20050  ply1remlem  20077  fta1b  20084  plyremlem  20213  aannenlem2  20238  aalioulem5  20245  aalioulem6  20246  aaliou  20247  aaliou3lem3  20253  psercnlem2  20332  psercnlem1  20333  pserdvlem1  20335  ptolemy  20396  quart1cl  20686  quartlem2  20690  quartlem3  20691  quartlem4  20692  jensenlem2  20818  emcllem7  20832  ftalem4  20850  basellem2  20856  perfectlem1  21005  dchrelbasd  21015  dchrmulcl  21025  dchrinv  21037  lgsdchr  21124  pntlemd  21280  pntlemc  21281  pntlemb  21283  pntlemg  21284  usgra2edg  21394  wlkbprop  21526  wlkonwlk  21527  spthispth  21565  pthdepisspth  21566  isspthonpth  21576  1pthon  21583  constr2trl  21591  2pthon  21594  wlkdvspthlem  21599  wlkdvspth  21600  cyclispthon  21612  fargshiftf1  21616  constr3lem4  21626  constr3lem5  21627  constr3trllem1  21629  constr3trllem2  21630  constr3trl  21638  constr3pth  21639  constr3cyclp  21641  4cycl4dv  21646  vdgr0  21663  vdusgraval  21670  vdgrnn0pnf  21672  eupatrl  21682  grpoidinvlem2  21785  grpoidval  21796  grpoidinv2  21798  grpoinv  21807  grpoinvid1  21810  grpoinvid2  21811  grpolcan  21813  grpo2inv  21819  grpomuldivass  21829  grponpncan  21835  ablo4  21867  ablodivdiv4  21871  ablonnncan  21873  ablonnncan1  21875  ismndo1  21924  isrngod  21959  rngolz  21981  rngorz  21982  cnrngo  21983  vc0  22040  vcoprne  22050  isnvi  22084  nvmdi  22123  nvsubadd  22128  nvnpcan  22133  nvmeq0  22137  nvabs  22154  sspg  22219  ssps  22221  lno0  22249  nmoub3i  22266  nmblolbii  22292  ubthlem1  22364  minvecolem1  22368  elunop2  23508  pjclem4  23694  pj3si  23702  stlei  23735  csmdsymi  23829  atexch  23876  atcvatlem  23880  atcvat4i  23892  cdj3i  23936  iocinioc2  24134  xrstos  24193  ofldsqr  24232  ofldchr  24236  unitdivcld  24291  rnlogblem  24391  esumpcvgval  24460  pwsiga  24505  prsiga  24506  sigainb  24511  insiga  24512  isrnmeas  24546  measres  24568  measdivcstOLD  24570  measdivcst  24571  imambfm  24604  dya2iocnrect  24623  sibf0  24641  sibfof  24646  ballotlemsup  24754  subfacp1lem1  24857  subfacp1lem2a  24858  iccllyscon  24929  cvmsi  24944  cvmlift2lem10  24991  relexpindlem  25131  fprodeq0  25291  poseq  25520  wfrlem15  25544  elno2  25601  brbtwn2  25836  colinearalg  25841  ax5seg  25869  axlowdim  25892  axcontlem2  25896  axcontlem4  25898  axcontlem9  25903  axcontlem10  25904  axcontlem12  25906  5segofs  25932  cgrextend  25934  segconeq  25936  segconeu  25937  trisegint  25954  fvtransport  25958  ifscgr  25970  cgrxfr  25981  btwnxfr  25982  lineext  26002  brofs2  26003  brifs2  26004  linecgr  26007  lineid  26009  btwnconn1lem4  26016  btwnconn1lem7  26019  btwnconn1lem8  26020  btwnconn1lem9  26021  btwnconn1lem11  26023  btwnconn1lem12  26024  btwnconn1lem13  26025  btwnconn1lem14  26026  btwnconn3  26029  brsegle2  26035  broutsideof2  26048  btwnoutside  26051  broutsideof3  26052  outsideoftr  26055  outsideofeu  26057  liness  26071  lineunray  26073  ellines  26078  supaddc  26228  supadd  26229  mblfinlem2  26235  ismblfin  26237  itg2addnclem2  26247  ftc1anclem7  26276  ftc1anc  26278  tailfb  26397  indexa  26426  seqpo  26442  nninfnub  26446  sstotbnd2  26474  rngohomsub  26580  crngm4  26604  igenval2  26667  prnc  26668  isfldidl  26669  ismrc  26746  jm2.17a  27016  congabseq  27030  jm2.18  27050  jm2.26a  27062  jm2.26lem3  27063  jm2.16nn0  27066  jm2.27c  27069  pmtrfrn  27368  pmtrfb  27374  psgnunilem2  27386  psgnunilem3  27387  deg1mhm  27494  pm13.194  27580  ubelsupr  27658  cncmpmax  27670  rfcnpre3  27671  rfcnpre4  27672  fmuldfeq  27680  fmul01lt1lem1  27681  fmul01lt1lem2  27682  climinf  27699  stoweidlem3  27719  stoweidlem14  27730  stoweidlem15  27731  stoweidlem20  27736  stoweidlem23  27739  stoweidlem26  27742  stoweidlem29  27745  stoweidlem34  27750  stoweidlem38  27754  stoweidlem39  27755  stoweidlem43  27759  stoweidlem44  27760  stoweidlem50  27766  stoweidlem51  27767  stoweidlem56  27772  stoweidlem59  27775  sigarcol  27821  sharhght  27822  cevathlem2  27825  cevath  27826  ndmaovdistr  28038  el2xptp0  28051  oteqimp  28053  2leaddle2  28077  elfzmlbm  28090  elfzmlbp  28091  elfzelfzelfz  28093  elfz0fzfz0  28098  fz0fzelfz0  28102  fz0fzdiffz0  28103  ubmelfzo  28109  ubmelm1fzo  28110  fzo1fzo0n0  28111  subsubelfzo0  28118  nn0nndivcl  28119  nn0ge0div  28120  flltdivnn0lt  28125  2submod  28130  swrd0  28155  swrdvalodm2  28160  swrd0swrd  28163  swrdswrdlem  28164  swrd0swrdid  28166  swrdswrd0  28167  swrdccatin1  28171  swrdccatin12lem3a  28174  swrdccatin12lem3b  28175  swrdccatin2  28176  swrdccatin12lem3c  28177  swrdccatin12lem3  28178  swrdccatin12lem4  28179  swrdccatin12  28180  swrdccat3  28181  swrdccat  28182  modprm0  28194  cshwoor  28203  cshwidx  28208  cshwidxmod  28209  cshwidxn  28213  2cshw1lem1  28214  2cshw1lem2  28215  2cshw1lem3  28216  2cshw2lem1  28218  2cshw2lem2  28219  2cshw2lem3  28220  2cshwid  28224  cshweqdif2  28233  cshweqdif2s  28234  usgra2pthspth  28258  usgra2wlkspth  28261  usgra2pthlem1  28263  usgra2pth  28264  usgra2adedgspth  28268  usgra2adedgwlk  28269  usgra2adedgwlkon  28270  el2wlkonot  28289  el2spthonot  28290  el2spthonot0  28291  el2wlkonotot0  28292  2wlkonot3v  28295  2spthonot3v  28296  usg2wotspth  28304  usg2spthonot0  28309  usg2spthonot1  28310  usgfidegfi  28313  3vfriswmgra  28332  2pthfrgra  28338  3cyclfrgra  28342  frgranbnb  28347  vdn0frgrav2  28351  vdn1frgrav2  28353  vdgfrgragt2  28355  frgrancvvdeqlem3  28358  frgrancvvdeqlemC  28365  frgrancvvdeq  28368  frgrawopreglem5  28374  frgrawopreg  28375  frg2woteu  28381  frg2woteqm  28385  frg2woteq  28386  usg2spot2nb  28391  usgreg2spot  28393  4animp1  28517  bnj951  29083  bnj605  29215  bnj607  29224  bnj908  29239  bnj1001  29266  bnj1110  29288  bnj1128  29296  islshpcv  29788  isopiN  29916  latm12  29965  omllaw5N  29982  cmtcomlemN  29983  cmtbr3N  29989  omlfh3N  29994  atlen0  30045  cvlsupr2  30078  hlomcmat  30099  exatleN  30138  2llnneN  30143  cvrexchlem  30153  cvratlem  30155  atcvrj2b  30166  atltcvr  30169  atlelt  30172  atexchcvrN  30174  cvrat4  30177  2atjm  30179  atbtwnexOLDN  30181  atbtwnex  30182  4noncolr3  30187  3dimlem2  30193  3dimlem3  30195  3dimlem3OLDN  30196  3dimlem4  30198  3dimlem4OLDN  30199  3dim1  30201  3dim2  30202  3dim3  30203  1cvrat  30210  ps-2b  30216  3atlem4  30220  3atlem5  30221  3atlem6  30222  llnexatN  30255  llncvrlpln2  30291  2llnmj  30294  lplnexatN  30297  4atlem3a  30331  4atlem10  30340  4atlem11b  30342  4atlem11  30343  4atlem12b  30345  4atlem12  30346  lplncvrlvol2  30349  2lplnja  30353  2lplnj  30354  2lplnmj  30356  dalemswapyz  30390  dalemrot  30391  dalemswapyzps  30424  dalemrotps  30425  dalem51  30457  dalem52  30458  dath2  30471  lneq2at  30512  lncvrelatN  30515  cdlema1N  30525  cdlema2N  30526  cdlemblem  30527  paddval  30532  padd01  30545  padd02  30546  paddss12  30553  paddasslem2  30555  paddasslem4  30557  paddasslem6  30559  paddasslem9  30562  paddasslem10  30563  paddasslem12  30565  paddasslem15  30568  pmodlem1  30580  pmod2iN  30583  pmodN  30584  pmapjat1  30587  dalawlem1  30605  paddunN  30661  poml4N  30687  poml5N  30688  osumcllem6N  30695  pexmidlem6N  30709  pl42lem2N  30714  lhpexle1lem  30741  lhpexle1  30742  lhpexle2lem  30743  lhpexle3lem  30745  lhpmcvr5N  30761  lhpmcvr6N  30762  4atexlemswapqr  30797  4atexlemex6  30808  cdlemd2  30933  cdlemd5  30936  cdleme01N  30955  cdleme3b  30963  cdleme20i  31051  cdleme20m  31057  cdleme21d  31064  cdleme21e  31065  cdleme21i  31069  cdleme21j  31070  cdleme21  31071  cdleme22cN  31076  cdleme22f2  31081  cdleme24  31086  cdleme26f2ALTN  31098  cdleme26f2  31099  cdleme27a  31101  cdleme28a  31104  cdleme43fsv1snlem  31154  cdleme37m  31196  cdleme38m  31197  cdleme38n  31198  cdleme40n  31202  cdleme42mgN  31222  cdleme46f2g2  31227  cdleme46f2g1  31228  cdlemf1  31295  cdlemftr2  31300  cdlemg17pq  31406  cdlemg29  31439  cdlemg33b  31441  cdlemi  31554  tendocan  31558  cdlemk6  31571  cdlemk7  31582  cdlemk12  31584  cdlemk16  31591  cdlemk5u  31595  cdlemk18  31602  cdlemk19  31603  cdlemk7u  31604  cdlemk11u  31605  cdlemk12u  31606  cdlemk21N  31607  cdlemk20  31608  cdlemk7u-2N  31622  cdlemk11u-2N  31623  cdlemk12u-2N  31624  cdlemk21-2N  31625  cdlemk20-2N  31626  cdlemk22  31627  cdlemk31  31630  cdlemk23-3  31636  cdlemk24-3  31637  cdlemk25-3  31638  cdlemk26b-3  31639  cdlemk26-3  31640  cdlemk27-3  31641  cdlemk28-3  31642  cdlemk33N  31643  cdlemk34  31644  cdlemky  31660  cdlemk11ta  31663  cdlemk19ylem  31664  cdlemk35s-id  31672  cdlemk39s-id  31674  cdlemk19xlem  31676  cdlemk11tc  31679  cdlemk11t  31680  cdlemk47  31683  cdlemk53b  31690  cdlemk53  31691  cdlemkyyN  31696  cdlemk55u1  31699  cdlemk19u1  31703  erng1r  31729  dvalveclem  31760  diclspsn  31929  dihmeetlem20N  32061  islpoldN  32219  lpolconN  32222
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