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

Theorem jctil 537
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 532 1  |-  ( ph  ->  ( ch  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
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 185  df-an 371
This theorem is referenced by:  jctl  541  nic-ax  1506  nic-axALT  1507  unidif  4285  iunxdif2  4380  exss  4719  xpiindi  5148  relssres  5321  nfunsn  5903  exfo  6050  fliftcnv  6210  f1oweALT  6783  fo1stres  6823  fo2ndres  6824  dftpos3  6991  tfrlem10  7074  odi  7246  omabs  7314  elixpsn  7527  sbthlem2  7647  sbthlem3  7648  fodomr  7687  mapxpen  7702  phplem2  7716  pssnn  7757  oieu  7982  inf3lem6  8067  acni3  8445  dfacacn  8538  kmlem1  8547  cflm  8647  cfsuc  8654  hsmexlem2  8824  hsmexlem4  8826  hsmexlem5  8827  axdc3lem4  8850  axcclem  8854  brdom5  8924  brdom4  8925  konigthlem  8960  alephval2  8964  alephmul  8970  wunex3  9136  reclem2pr  9443  suplem2pr  9448  lemulge11  10425  nn0ge2m1nn  10882  0mod  12030  1mod  12031  fzennn  12081  hashbclem  12505  hash2prd  12522  hashge2el2dif  12525  wrdlenge2n0  12585  elovmptnn0wrd  12592  swrdnd  12668  2swrdeqwrdeq  12690  repswcshw  12792  s2f1o  12876  f1oun2prg  12877  resqrex  13096  demoivreALT  13948  pcdiv  14388  invsym2  15179  idghm  16409  gaid  16464  subrgid  17558  lbsextlem1  17931  mulgghm2  18658  mulgghm2OLD  18661  smadiadet  19299  pmatcollpw3fi  19413  topcld  19663  ntrss  19683  restcld  19800  xkocnv  20441  fbssfi  20464  isfild  20485  alexsublem  20670  alexsubALTlem4  20676  metrest  21153  dscopn  21220  reconnlem1  21457  cphsubrglem  21750  itgcnlem  22322  vieta1  22834  jensen  23444  axlowdimlem6  24377  axlowdimlem7  24378  axlowdimlem16  24387  axlowdimlem17  24388  cusgrafilem1  24606  0trlon  24677  2trllemE  24682  1pthon2v  24722  3v3e3cycl1  24771  4cycl4v4e  24793  4cycl4dv  24794  1conngra  24802  clwwlkf1  24923  usg2cwwkdifex  24948  rusgranumwlklem4  25079  rusgranumwwlkg  25086  numclwwlkovf2ex  25213  numclwwlkqhash  25227  nvge0  25704  ipval2  25744  sspg  25768  ssps  25770  sspmlem  25772  blocni  25847  ubthlem1  25913  bcsiALT  26223  ocsh  26328  chabs2  26562  pjoml6i  26634  osumcor2i  26689  nmopcoi  27141  opsqrlem6  27191  stlei  27286  mdslmd1lem1  27371  mdslmd2i  27376  atcvat3i  27442  atcvat4i  27443  sumdmdlem2  27465  dmdbr5ati  27468  xdivpnfrp  27789  oduprs  27804  tpr2rico  28055  ballotlemfp1  28627  ballotlemfc0  28628  ballotlemfcc  28629  ballotlemsup  28640  wfr3g  29559  frr3g  29603  nodense  29666  nobndlem1  29669  nobnddown  29678  nofulllem3  29681  mblfinlem1  30256  mblfinlem2  30257  mblfinlem3  30258  mblfinlem4  30259  ismblfin  30260  trer  30339  filnetlem3  30403  filnetlem4  30404  prter1  30825  irrapx1  30968  dfacbasgrp  31261  dgraalem  31298  dgraaub  31301  dvsconst  31439  dvsid  31440  dvsef  31441  islptre  31828  wallispilem1  32050  fourierdlem52  32144  usgsizedg  32657  usgsizedgALT  32658  usgsizedgALT2  32659  lincext1  33199  linds0  33210  lindsrng01  33213  lmod1lem3  33234  bnj545  34096  bnj548  34098  pmapsub  35635  cotrtrclfv  37972
  Copyright terms: Public domain W3C validator