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  1480  nic-axALT  1481  unidif  4130  iunxdif2  4223  exss  4560  xpiindi  4980  relssres  5152  nfunsn  5726  exfo  5866  fliftcnv  6009  f1oweALT  6566  fo1stres  6605  fo2ndres  6606  dftpos3  6768  tfrlem10  6851  odi  7023  omabs  7091  elixpsn  7307  sbthlem2  7427  sbthlem3  7428  fodomr  7467  mapxpen  7482  phplem2  7496  pssnn  7536  oieu  7758  inf3lem6  7844  acni3  8222  dfacacn  8315  kmlem1  8324  cflm  8424  cfsuc  8431  hsmexlem2  8601  hsmexlem4  8603  hsmexlem5  8604  axdc3lem4  8627  axcclem  8631  brdom5  8701  brdom4  8702  konigthlem  8737  alephval2  8741  alephmul  8747  wunex3  8913  reclem2pr  9222  suplem2pr  9227  lemulge11  10196  0mod  11744  1mod  11745  fzennn  11795  hash2prd  12186  hashge2el2dif  12189  hashbclem  12210  wrdlenge2n0  12266  swrdlend  12330  swrd0  12332  2swrdeqwrdeq  12352  repswcshw  12451  s2f1o  12531  f1oun2prg  12532  resqrex  12745  demoivreALT  13490  pcdiv  13924  invsym2  14706  idghm  15767  gaid  15822  subrgid  16872  lbsextlem1  17244  mulgghm2  17930  mulgghm2OLD  17933  smadiadet  18481  topcld  18644  ntrss  18664  restcld  18781  xkocnv  19392  fbssfi  19415  isfild  19436  alexsublem  19621  alexsubALTlem4  19627  metrest  20104  dscopn  20171  reconnlem1  20408  cphsubrglem  20701  itgcnlem  21272  vieta1  21783  jensen  22387  axlowdimlem6  23198  axlowdimlem7  23199  axlowdimlem16  23208  axlowdimlem17  23209  cusgrafilem1  23392  0trlon  23452  2trllemE  23457  1pthon2v  23497  3v3e3cycl1  23535  4cycl4v4e  23557  4cycl4dv  23558  1conngra  23566  nvge0  24067  ipval2  24107  sspg  24131  ssps  24133  sspmlem  24135  blocni  24210  ubthlem1  24276  bcsiALT  24586  ocsh  24691  chabs2  24925  pjoml6i  24997  osumcor2i  25052  nmopcoi  25504  opsqrlem6  25554  stlei  25649  mdslmd1lem1  25734  mdslmd2i  25739  atcvat3i  25805  atcvat4i  25806  sumdmdlem2  25828  dmdbr5ati  25831  xdivpnfrp  26113  tpr2rico  26347  ballotlemfp1  26879  ballotlemfc0  26880  ballotlemfcc  26881  ballotlemsup  26892  wfr3g  27728  frr3g  27772  nodense  27835  nobndlem1  27838  nobnddown  27847  nofulllem3  27850  mblfinlem1  28433  mblfinlem2  28434  mblfinlem3  28435  mblfinlem4  28436  ismblfin  28437  trer  28516  fnessref  28570  refssfne  28571  filnetlem3  28606  filnetlem4  28607  prter1  29029  irrapx1  29174  dfacbasgrp  29469  dgraalem  29507  dgraaub  29510  dvsconst  29609  dvsid  29610  dvsef  29611  wallispilem1  29865  elovmptnn0wrd  30262  clwwlkf1  30463  usg2cwwkdifex  30500  rusgranumwlklem4  30575  rusgranumwwlkg  30582  numclwwlkovf2ex  30684  numclwwlkqhash  30698  lincext1  30993  linds0  31004  lindsrng01  31007  lmod1lem3  31036  bnj545  31893  bnj548  31895  pmapsub  33417
  Copyright terms: Public domain W3C validator