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

Theorem jctil 544
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 539 1  |-  ( ph  ->  ( ch  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  jctl  548  nic-ax  1560  nic-axALT  1561  unidif  4201  iunxdif2  4296  exss  4636  xpiindi  4948  relssres  5120  nfunsn  5879  exfo  6024  fliftcnv  6190  f1oweALT  6765  fo1stres  6805  fo2ndres  6806  dftpos3  6978  wfr3g  7021  tfrlem10  7092  odi  7267  omabs  7335  elixpsn  7548  sbthlem2  7670  sbthlem3  7671  fodomr  7710  mapxpen  7725  phplem2  7739  pssnn  7777  oieu  8041  inf3lem6  8125  acni3  8465  dfacacn  8558  kmlem1  8567  cflm  8667  cfsuc  8674  hsmexlem2  8844  hsmexlem4  8846  hsmexlem5  8847  axdc3lem4  8870  axcclem  8874  brdom5  8944  brdom4  8945  konigthlem  8980  alephval2  8984  alephmul  8990  wunex3  9153  reclem2pr  9460  suplem2pr  9465  lemulge11  10456  nn0ge2m1nn  10924  0mod  12122  1mod  12123  fzennn  12175  hashbclem  12610  hashge2el2dif  12632  wrdlenge2n0  12701  elovmptnn0wrd  12708  swrdnd  12787  2swrdeqwrdeq  12808  repswcshw  12910  s2f1o  13009  f1oun2prg  13010  cotrtrclfv  13087  resqrex  13325  demoivreALT  14266  pcdiv  14813  prmodvdslcmf  15016  prmordvdslcmfOLD  15030  invsym2  15679  idghm  16909  gaid  16964  subrgid  18021  lbsextlem1  18392  mulgghm2  19079  smadiadet  19706  pmatcollpw3fi  19820  topcld  20061  ntrss  20081  restcld  20199  xkocnv  20840  fbssfi  20863  isfild  20884  alexsublem  21070  alexsubALTlem4  21076  metrest  21550  dscopn  21599  reconnlem1  21855  cphsubrglem  22166  itgcnlem  22759  vieta1  23277  jensen  23926  axlowdimlem6  24989  axlowdimlem7  24990  axlowdimlem16  24999  axlowdimlem17  25000  cusgrafilem1  25219  0trlon  25290  2trllemE  25295  1pthon2v  25335  3v3e3cycl1  25384  4cycl4v4e  25406  4cycl4dv  25407  1conngra  25415  clwwlkf1  25536  usg2cwwkdifex  25561  rusgranumwlklem4  25692  rusgranumwwlkg  25699  numclwwlkovf2ex  25826  numclwwlkqhash  25840  nvge0  26315  ipval2  26355  sspg  26379  ssps  26381  sspmlem  26383  blocni  26458  ubthlem1  26524  bcsiALT  26844  ocsh  26948  chabs2  27182  pjoml6i  27254  osumcor2i  27309  nmopcoi  27760  opsqrlem6  27810  stlei  27905  mdslmd1lem1  27990  mdslmd2i  27995  atcvat3i  28061  atcvat4i  28062  sumdmdlem2  28084  dmdbr5ati  28087  xdivpnfrp  28410  oduprs  28425  tpr2rico  28725  ballotlemfp1  29330  ballotlemfc0  29331  ballotlemfcc  29332  ballotlemsup  29343  ballotlemsupOLD  29381  bnj545  29712  bnj548  29714  fv1stcnv  30428  fv2ndcnv  30429  frr3g  30519  nodense  30584  nobndlem1  30587  nobnddown  30596  nofulllem3  30599  trer  30978  filnetlem3  31042  filnetlem4  31043  phpreu  31931  poimirlem16  31958  poimirlem17  31959  poimirlem19  31961  poimirlem20  31962  poimirlem26  31968  mblfinlem1  31979  mblfinlem2  31980  mblfinlem3  31981  mblfinlem4  31982  ismblfin  31983  prter1  32453  pmapsub  33335  irrapx1  35674  dfacbasgrp  35969  dgraalem  36009  dgraalemOLD  36010  dgraaub  36015  dgraaubOLD  36016  dvsconst  36680  dvsid  36681  dvsef  36682  islptre  37741  wallispilem1  37984  fourierdlem52  38079  ovnhoilem1  38486  gbogt5  38954  gboage9  38956  nnsum3primesprm  38976  nnsum3primesgbe  38978  bgoldbnnsum3prm  38990  tgoldbachlt  39000  usgr2v1e2w  39429  hashnbusgrvd  39667  0edg0rgr  39690  usgr2wlkspthlem2  39842  0pthon-av  39895  usgsizedg  40032  usgsizedgALT  40033  usgsizedgALT2  40034  lincext1  40572  linds0  40583  lindsrng01  40586  lmod1lem3  40607
  Copyright terms: Public domain W3C validator