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  5098  tz7.49  6473  oeeulem  6615  domss2  7036  intrnfi  7186  dffi2  7192  elfiun  7199  hartogslem1  7273  wemaplem2  7278  oemapvali  7402  cfss  7907  cofsmo  7911  axdc3lem4  8095  axdc4lem  8097  fpwwe2lem6  8273  fpwwe2lem13  8280  canth4  8285  intwun  8373  r1limwun  8374  wunex2  8376  tskwun  8422  gruwun  8451  intgru  8452  wfgru  8454  grutsk1  8459  le2tri3i  8965  ledivmulOLD  9646  supmul1  9735  supmullem2  9737  eluzp1p1  10269  peano2uz  10288  rpnnen1lem5  10362  ixxun  10688  elioc2  10729  elico2  10730  elicc2  10731  iccsupr  10752  iccsplit  10784  fzrev3  10865  fseq1p1m1  10873  elfzo2  10894  elfzo0  10920  intfrac2  10978  intfracq  10979  seqf1olem2  11102  remullem  11629  sqr0lem  11742  sqrlem3  11746  resqreu  11754  resqrcl  11755  sqrneglem  11768  sqreulem  11859  eqsqrd  11867  climsup  12159  fsumcvg3  12218  supcvg  12330  mertenslem2  12357  sin02gt0  12488  ruclem1  12525  ruclem2  12526  ruclem11  12534  gcdcllem3  12708  rppwr  12752  qredeq  12801  maxprmfct  12808  pythagtriplem6  12890  pythagtriplem7  12891  pythagtriplem19  12902  pclem  12907  prmreclem1  12979  ramcl  13092  iscatd2  13599  issubc3  13739  prsref  14082  posref  14101  isposd  14105  isposi  14106  latjlej1  14187  latmlem1  14203  latledi  14211  latj32  14219  mod2ile  14228  lubss  14241  pslem  14331  letsr  14365  0mhm  14451  resmhm  14452  resmhm2  14453  resmhm2b  14454  mhmco  14455  prdspjmhm  14459  pwsdiagmhm  14461  pwsco1mhm  14462  pwsco2mhm  14463  frmdup1  14502  grpinvid1  14546  grpinvid2  14547  grplcan  14550  issubg2  14652  issubg4  14654  ghmmhm  14709  cayley  14805  lsmelvali  14977  pj1id  15024  frgpmhm  15090  mulgmhm  15143  dmdprdsplit  15298  ablfac1lem  15319  ablfac2  15340  rnglz  15393  rngrz  15394  isrhm2d  15522  subrgunit  15579  issubrg2  15581  islmodd  15649  islmhm2  15811  islmhmd  15812  reslmhm  15825  islbs2  15923  islbs3  15924  isassad  16079  isphld  16574  iscldtop  16848  iscnp2  16985  cnpnei  17009  cnpco  17012  hausnei2  17097  nconsubb  17165  nlly2i  17218  elptr  17284  upxp  17333  elmptrab2  17539  opnfbas  17553  isfil2  17567  isfild  17569  infil  17574  fsubbas  17578  neifil  17591  fbasrn  17595  rnelfmlem  17663  fmfnfmlem4  17668  fmfnfm  17669  flimclslem  17695  flimsncls  17697  istgp2  17790  tsmsfbas  17826  tmslem  18044  stdbdmopn  18080  isngp4  18149  sranlm  18211  nlmtlm  18220  lssnlm  18227  nmoleub  18256  qdensere  18295  iirev  18443  iihalf1  18445  iihalf2  18447  iimulcl  18451  icoopnst  18453  iocopnst  18454  evth  18473  pcoptcl  18535  pcorevcl  18539  nmhmcn  18617  cphsubrglem  18629  tchcph  18683  cmetcaulem  18730  hlprlem  18800  minveclem1  18804  minveclem3b  18808  ivthlem2  18828  ivthlem3  18829  vitalilem2  18980  mbfsup  19035  i1fd  19052  itg2seq  19113  itg2mono  19124  itgsplitioo  19208  dvfsumlem4  19392  dvfsumrlim3  19396  evlslem1  19415  mdegaddle  19476  mdegmullem  19480  ply1divmo  19537  ply1remlem  19564  fta1b  19571  plyremlem  19700  aannenlem2  19725  aalioulem5  19732  aalioulem6  19733  aaliou  19734  aaliou3lem3  19740  psercnlem2  19816  psercnlem1  19817  pserdvlem1  19819  ptolemy  19880  quart1cl  20166  quartlem2  20170  quartlem3  20171  quartlem4  20172  jensenlem2  20298  emcllem7  20311  ftalem4  20329  basellem2  20335  perfectlem1  20484  dchrelbasd  20494  dchrmulcl  20504  dchrinv  20516  lgsdchr  20603  pntlemd  20759  pntlemc  20760  pntlemb  20762  pntlemg  20763  grpoidinvlem2  20888  grpoidval  20899  grpoidinv2  20901  grpoinv  20910  grpoinvid1  20913  grpoinvid2  20914  grpolcan  20916  grpo2inv  20922  grpomuldivass  20932  grponpncan  20938  ablo4  20970  ablodivdiv4  20974  ablonnncan  20976  ablonnncan1  20978  ismndo1  21027  isrngod  21062  rngolz  21084  rngorz  21085  cnrngo  21086  vc0  21141  vcoprne  21151  isnvi  21185  nvmdi  21224  nvsubadd  21229  nvnpcan  21234  nvmeq0  21238  nvabs  21255  sspg  21320  ssps  21322  lno0  21350  nmoub3i  21367  nmblolbii  21393  ubthlem1  21465  minvecolem1  21469  elunop2  22609  pjclem4  22795  pj3si  22803  stlei  22836  csmdsymi  22930  atexch  22977  atcvatlem  22981  atcvat4i  22993  cdj3i  23037  bcm1n  23048  ballotlemsup  23079  ballotlemsdom  23086  lt2addrd  23264  xlt2addrd  23268  eliccelico  23285  elicoelioo  23286  iocinioc2  23287  elfzo1  23294  unitdivcld  23300  cnre2csqlem  23309  tpr2rico  23311  disjabrex  23374  disjabrexf  23375  rnlogblem  23416  rnlogbval  23417  nnlogbexp  23421  esumpcvgval  23461  pwsiga  23506  prsiga  23507  sigainb  23512  insiga  23513  isrnmeas  23546  measres  23564  measdivcstOLD  23566  measdivcst  23567  cntmeas  23568  imambfm  23582  dya2iocseg  23594  probdsb  23640  dstrvprob  23687  subfacp1lem1  23725  subfacp1lem2a  23726  iccllyscon  23796  cvmsi  23811  cvmlift2lem10  23858  vdgr0  23907  relexpindlem  24051  poseq  24324  wfrlem15  24341  elno2  24379  brbtwn2  24605  colinearalg  24610  ax5seg  24638  axlowdim  24661  axcontlem2  24665  axcontlem4  24667  axcontlem9  24672  axcontlem10  24673  axcontlem12  24675  5segofs  24701  cgrextend  24703  segconeq  24705  segconeu  24706  trisegint  24723  fvtransport  24727  ifscgr  24739  cgrxfr  24750  btwnxfr  24751  lineext  24771  brofs2  24772  brifs2  24773  linecgr  24776  lineid  24778  btwnconn1lem4  24785  btwnconn1lem7  24788  btwnconn1lem8  24789  btwnconn1lem9  24790  btwnconn1lem11  24792  btwnconn1lem12  24793  btwnconn1lem13  24794  btwnconn1lem14  24795  btwnconn3  24798  brsegle2  24804  broutsideof2  24817  btwnoutside  24820  broutsideof3  24821  outsideoftr  24824  outsideofeu  24826  liness  24840  lineunray  24842  ellines  24847  supaddc  24995  supadd  24996  itg2addnclem2  25004  iccss3  25237  cljo  25289  clme  25290  int2pre  25340  definc  25382  dfps2  25392  reacomsmgrp1  25446  reacomsmgrp3  25448  reacomsmgrp4  25449  resgcom  25454  grpodrcan  25478  grpodlcan  25479  rltrran  25517  rltrooo  25518  dblsubvec  25577  mvecrtol2  25580  glmrngo  25585  svli2  25587  vri  25595  truni1  25608  cbci  25611  mslb1  25710  trnij  25718  xrletr2  25721  flfnein  25724  lvsovso  25729  lvsovso3  25731  addcanri  25769  distmlva  25791  distsava  25792  icccon2  25803  icccon4  25805  dualalg  25885  dualded  25886  homgrf  25905  imonclem  25916  ismonc  25917  idmon  25920  immon  25921  iepiclem  25926  isepic  25927  idfisf  25944  idsubfun  25961  tartarmap  25991  fnctartar  26010  fnctartar2  26011  setiscat  26082  bisig0  26165  isconcl6a  26206  isside  26269  bosser  26270  pdiveql  26271  tailfb  26429  indexa  26515  seqpo  26560  nninfnub  26564  sstotbnd2  26601  rngohomsub  26707  crngm4  26731  igenval2  26794  prnc  26795  isfldidl  26796  ismrc  26879  jm2.17a  27150  congabseq  27164  jm2.18  27184  jm2.26a  27196  jm2.26lem3  27197  jm2.16nn0  27200  jm2.27c  27203  pmtrfrn  27503  pmtrfb  27509  psgnunilem2  27521  psgnunilem3  27522  deg1mhm  27629  pm13.194  27715  ubelsupr  27794  fcnre  27799  fnchoice  27803  refsumcn  27804  cncmpmax  27806  rfcnpre3  27807  rfcnpre4  27808  refsum2cnlem1  27811  fmul01  27813  fmulcl  27814  fmuldfeq  27816  fmul01lt1lem1  27817  fmul01lt1lem2  27818  climinf  27835  climsuselem1  27836  climsuse  27837  ibliccsinexp  27848  itgsinexplem1  27851  itgsinexp  27852  stoweidlem1  27853  stoweidlem3  27855  stoweidlem5  27857  stoweidlem7  27859  stoweidlem10  27862  stoweidlem11  27863  stoweidlem13  27865  stoweidlem14  27866  stoweidlem15  27867  stoweidlem16  27868  stoweidlem17  27869  stoweidlem18  27870  stoweidlem19  27871  stoweidlem20  27872  stoweidlem21  27873  stoweidlem22  27874  stoweidlem23  27875  stoweidlem24  27876  stoweidlem25  27877  stoweidlem26  27878  stoweidlem28  27880  stoweidlem29  27881  stoweidlem31  27883  stoweidlem32  27884  stoweidlem34  27886  stoweidlem36  27888  stoweidlem37  27889  stoweidlem38  27890  stoweidlem39  27891  stoweidlem40  27892  stoweidlem41  27893  stoweidlem42  27894  stoweidlem43  27895  stoweidlem44  27896  stoweidlem45  27897  stoweidlem46  27898  stoweidlem47  27899  stoweidlem48  27900  stoweidlem49  27901  stoweidlem50  27902  stoweidlem51  27903  stoweidlem52  27904  stoweidlem53  27905  stoweidlem54  27906  stoweidlem55  27907  stoweidlem56  27908  stoweidlem57  27909  stoweidlem58  27910  stoweidlem59  27911  stoweidlem60  27912  stoweidlem61  27913  stoweidlem62  27914  stoweid  27915  wallispilem1  27917  wallispilem3  27919  wallispilem4  27920  wallispilem5  27921  wallispi  27922  wallispi2lem1  27923  wallispi2  27925  stirlinglem3  27928  stirlinglem5  27930  stirlinglem6  27931  stirlinglem10  27935  sigarcol  27957  sharhght  27958  cevathlem2  27961  cevath  27962  ndmaovdistr  28175  elfznelfzo  28213  wlkbprop  28333  wlkonwlk  28334  spthispth  28359  pthdepisspth  28360  wlkdvspthlem  28365  wlkdvspth  28366  cyclispthon  28378  fargshiftf1  28382  eupatrl  28385  constr3lem4  28393  constr3lem5  28394  constr3trllem1  28396  constr3trllem2  28397  constr3trl  28405  constr3pth  28406  constr3cyclp  28408  4cycl4dv  28413  3vfriswmgra  28429  3cyclfrgra  28437  bnj951  29123  bnj605  29255  bnj607  29264  bnj908  29279  bnj1001  29306  bnj1110  29328  bnj1128  29336  islshpcv  29865  isopiN  29993  latm12  30042  omllaw5N  30059  cmtcomlemN  30060  cmtbr3N  30066  omlfh3N  30071  atlen0  30122  cvlsupr2  30155  hlomcmat  30176  exatleN  30215  2llnneN  30220  cvrexchlem  30230  cvratlem  30232  atcvrj2b  30243  atltcvr  30246  atlelt  30249  atexchcvrN  30251  cvrat4  30254  2atjm  30256  atbtwnexOLDN  30258  atbtwnex  30259  4noncolr3  30264  3dimlem2  30270  3dimlem3  30272  3dimlem3OLDN  30273  3dimlem4  30275  3dimlem4OLDN  30276  3dim1  30278  3dim2  30279  3dim3  30280  1cvrat  30287  ps-2b  30293  3atlem4  30297  3atlem5  30298  3atlem6  30299  llnexatN  30332  llncvrlpln2  30368  2llnmj  30371  lplnexatN  30374  4atlem3a  30408  4atlem10  30417  4atlem11b  30419  4atlem11  30420  4atlem12b  30422  4atlem12  30423  lplncvrlvol2  30426  2lplnja  30430  2lplnj  30431  2lplnmj  30433  dalemswapyz  30467  dalemrot  30468  dalemswapyzps  30501  dalemrotps  30502  dalem51  30534  dalem52  30535  dath2  30548  lneq2at  30589  lncvrelatN  30592  cdlema1N  30602  cdlema2N  30603  cdlemblem  30604  paddval  30609  padd01  30622  padd02  30623  paddss12  30630  paddasslem2  30632  paddasslem4  30634  paddasslem6  30636  paddasslem9  30639  paddasslem10  30640  paddasslem12  30642  paddasslem15  30645  pmodlem1  30657  pmod2iN  30660  pmodN  30661  pmapjat1  30664  dalawlem1  30682  paddunN  30738  poml4N  30764  poml5N  30765  osumcllem6N  30772  pexmidlem6N  30786  pl42lem2N  30791  lhpexle1lem  30818  lhpexle1  30819  lhpexle2lem  30820  lhpexle3lem  30822  lhpmcvr5N  30838  lhpmcvr6N  30839  4atexlemswapqr  30874  4atexlemex6  30885  cdlemd2  31010  cdlemd5  31013  cdleme01N  31032  cdleme3b  31040  cdleme20i  31128  cdleme20m  31134  cdleme21d  31141  cdleme21e  31142  cdleme21i  31146  cdleme21j  31147  cdleme21  31148  cdleme22cN  31153  cdleme22f2  31158  cdleme24  31163  cdleme26f2ALTN  31175  cdleme26f2  31176  cdleme27a  31178  cdleme28a  31181  cdleme43fsv1snlem  31231  cdleme37m  31273  cdleme38m  31274  cdleme38n  31275  cdleme40n  31279  cdleme42mgN  31299  cdleme46f2g2  31304  cdleme46f2g1  31305  cdlemf1  31372  cdlemftr2  31377  cdlemg17pq  31483  cdlemg29  31516  cdlemg33b  31518  cdlemi  31631  tendocan  31635  cdlemk6  31648  cdlemk7  31659  cdlemk12  31661  cdlemk16  31668  cdlemk5u  31672  cdlemk18  31679  cdlemk19  31680  cdlemk7u  31681  cdlemk11u  31682  cdlemk12u  31683  cdlemk21N  31684  cdlemk20  31685  cdlemk7u-2N  31699  cdlemk11u-2N  31700  cdlemk12u-2N  31701  cdlemk21-2N  31702  cdlemk20-2N  31703  cdlemk22  31704  cdlemk31  31707  cdlemk23-3  31713  cdlemk24-3  31714  cdlemk25-3  31715  cdlemk26b-3  31716  cdlemk26-3  31717  cdlemk27-3  31718  cdlemk28-3  31719  cdlemk33N  31720  cdlemk34  31721  cdlemky  31737  cdlemk11ta  31740  cdlemk19ylem  31741  cdlemk35s-id  31749  cdlemk39s-id  31751  cdlemk19xlem  31753  cdlemk11tc  31756  cdlemk11t  31757  cdlemk47  31760  cdlemk53b  31767  cdlemk53  31768  cdlemkyyN  31773  cdlemk55u1  31776  cdlemk19u1  31780  erng1r  31806  dvalveclem  31837  diclspsn  32006  dihmeetlem20N  32138  islpoldN  32296  lpolconN  32299
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