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

Theorem jctil 539
Description: Inference conjoining a theorem to left of consequent in an implication. (Contributed by NM, 31-Dec-1993.)
Hypotheses
Ref Expression
jctil.1  |-  ( ph  ->  ps )
jctil.2  |-  ch
Assertion
Ref Expression
jctil  |-  ( ph  ->  ( ch  /\  ps ) )

Proof of Theorem jctil
StepHypRef Expression
1 jctil.2 . . 3  |-  ch
21a1i 11 . 2  |-  ( ph  ->  ch )
3 jctil.1 . 2  |-  ( ph  ->  ps )
42, 3jca 534 1  |-  ( ph  ->  ( ch  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 188  df-an 372
This theorem is referenced by:  jctl  543  nic-ax  1550  nic-axALT  1551  unidif  4252  iunxdif2  4347  exss  4684  xpiindi  4989  relssres  5161  nfunsn  5912  exfo  6055  fliftcnv  6219  f1oweALT  6791  fo1stres  6831  fo2ndres  6832  dftpos3  7002  wfr3g  7045  tfrlem10  7116  odi  7291  omabs  7359  elixpsn  7572  sbthlem2  7692  sbthlem3  7693  fodomr  7732  mapxpen  7747  phplem2  7761  pssnn  7799  oieu  8063  inf3lem6  8147  acni3  8485  dfacacn  8578  kmlem1  8587  cflm  8687  cfsuc  8694  hsmexlem2  8864  hsmexlem4  8866  hsmexlem5  8867  axdc3lem4  8890  axcclem  8894  brdom5  8964  brdom4  8965  konigthlem  9000  alephval2  9004  alephmul  9010  wunex3  9173  reclem2pr  9480  suplem2pr  9485  lemulge11  10474  nn0ge2m1nn  10941  0mod  12134  1mod  12135  fzennn  12187  hashbclem  12619  hashge2el2dif  12641  wrdlenge2n0  12707  elovmptnn0wrd  12714  swrdnd  12790  2swrdeqwrdeq  12811  repswcshw  12913  s2f1o  13001  f1oun2prg  13002  cotrtrclfv  13076  resqrex  13314  demoivreALT  14254  pcdiv  14801  prmodvdslcmf  15004  prmordvdslcmfOLD  15018  invsym2  15667  idghm  16897  gaid  16952  subrgid  18009  lbsextlem1  18380  mulgghm2  19066  smadiadet  19693  pmatcollpw3fi  19807  topcld  20048  ntrss  20068  restcld  20186  xkocnv  20827  fbssfi  20850  isfild  20871  alexsublem  21057  alexsubALTlem4  21063  metrest  21537  dscopn  21586  reconnlem1  21842  cphsubrglem  22153  itgcnlem  22745  vieta1  23263  jensen  23912  axlowdimlem6  24975  axlowdimlem7  24976  axlowdimlem16  24985  axlowdimlem17  24986  cusgrafilem1  25205  0trlon  25276  2trllemE  25281  1pthon2v  25321  3v3e3cycl1  25370  4cycl4v4e  25392  4cycl4dv  25393  1conngra  25401  clwwlkf1  25522  usg2cwwkdifex  25547  rusgranumwlklem4  25678  rusgranumwwlkg  25685  numclwwlkovf2ex  25812  numclwwlkqhash  25826  nvge0  26301  ipval2  26341  sspg  26365  ssps  26367  sspmlem  26369  blocni  26444  ubthlem1  26510  bcsiALT  26830  ocsh  26934  chabs2  27168  pjoml6i  27240  osumcor2i  27295  nmopcoi  27746  opsqrlem6  27796  stlei  27891  mdslmd1lem1  27976  mdslmd2i  27981  atcvat3i  28047  atcvat4i  28048  sumdmdlem2  28070  dmdbr5ati  28073  xdivpnfrp  28409  oduprs  28424  tpr2rico  28726  ballotlemfp1  29332  ballotlemfc0  29333  ballotlemfcc  29334  ballotlemsup  29345  ballotlemsupOLD  29383  bnj545  29714  bnj548  29716  fv1stcnv  30429  fv2ndcnv  30430  frr3g  30520  nodense  30583  nobndlem1  30586  nobnddown  30595  nofulllem3  30598  trer  30977  filnetlem3  31041  filnetlem4  31042  phpreu  31893  poimirlem16  31920  poimirlem17  31921  poimirlem19  31923  poimirlem20  31924  poimirlem26  31930  mblfinlem1  31941  mblfinlem2  31942  mblfinlem3  31943  mblfinlem4  31944  ismblfin  31945  prter1  32419  pmapsub  33302  irrapx1  35642  dfacbasgrp  35937  dgraalem  35977  dgraalemOLD  35978  dgraaub  35983  dgraaubOLD  35984  dvsconst  36649  dvsid  36650  dvsef  36651  islptre  37639  wallispilem1  37867  fourierdlem52  37962  ovnhoilem1  38327  gbogt5  38733  gboage9  38735  nnsum3primesprm  38755  nnsum3primesgbe  38757  bgoldbnnsum3prm  38769  tgoldbachlt  38779  usgsizedg  39327  usgsizedgALT  39328  usgsizedgALT2  39329  lincext1  39869  linds0  39880  lindsrng01  39883  lmod1lem3  39904
  Copyright terms: Public domain W3C validator