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

Theorem jctil 524
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 519 1  |-  ( ph  ->  ( ch  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  jctl  526  nic-ax  1444  nic-axALT  1445  unidif  4007  iunxdif2  4099  exss  4386  xpiindi  4969  relssres  5142  nfunsn  5720  exfo  5846  fliftcnv  5992  f1oweALT  6033  fo1stres  6329  fo2ndres  6330  dftpos3  6456  tfrlem10  6607  odi  6781  omabs  6849  elixpsn  7060  sbthlem2  7177  sbthlem3  7178  fodomr  7217  mapxpen  7232  phplem2  7246  pssnn  7286  oieu  7464  inf3lem6  7544  acni3  7884  dfacacn  7977  kmlem1  7986  cflm  8086  cfsuc  8093  hsmexlem2  8263  hsmexlem4  8265  hsmexlem5  8266  axdc3lem4  8289  axcclem  8293  brdom5  8363  brdom4  8364  konigthlem  8399  alephval2  8403  alephmul  8409  wunex3  8572  reclem2pr  8881  suplem2pr  8886  lemulge11  9828  0mod  11227  1mod  11228  fzennn  11262  hashbclem  11656  s2f1o  11818  f1oun2prg  11819  resqrex  12011  demoivreALT  12757  pcdiv  13181  invsym2  13943  idghm  14976  gaid  15031  subrgid  15825  lbsextlem1  16185  mulgghm2  16741  topcld  17054  ntrss  17074  restcld  17190  xkocnv  17799  fbssfi  17822  isfild  17843  alexsublem  18028  alexsubALTlem4  18034  metrest  18507  dscopn  18574  reconnlem1  18810  cphsubrglem  19093  itgcnlem  19634  vieta1  20182  jensen  20780  cusgrafilem1  21441  0trlon  21501  2trllemE  21506  1pthon2v  21546  3v3e3cycl1  21584  4cycl4v4e  21606  4cycl4dv  21607  1conngra  21615  nvge0  22116  ipval2  22156  sspg  22180  ssps  22182  sspmlem  22184  blocni  22259  ubthlem1  22325  bcsiALT  22634  ocsh  22738  chabs2  22972  pjoml6i  23044  osumcor2i  23099  nmopcoi  23551  opsqrlem6  23601  stlei  23696  mdslmd1lem1  23781  mdslmd2i  23786  atcvat3i  23852  atcvat4i  23853  sumdmdlem2  23875  dmdbr5ati  23878  xdivpnfrp  24132  tpr2rico  24263  ballotlemfp1  24702  ballotlemfc0  24703  ballotlemfcc  24704  ballotlemsup  24715  wfr3g  25469  frr3g  25494  nodense  25557  nobndlem1  25560  nobnddown  25569  nofulllem3  25572  axlowdimlem6  25790  axlowdimlem7  25791  axlowdimlem16  25800  axlowdimlem17  25801  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  ismblfin  26146  trer  26209  fnessref  26263  refssfne  26264  filnetlem3  26299  filnetlem4  26300  prter1  26618  irrapx1  26781  dfacbasgrp  27141  dgraalem  27218  dgraaub  27221  dvsconst  27415  dvsid  27416  dvsef  27417  wallispilem1  27681  swrdltnd  28000  bnj545  28972  bnj548  28974  pmapsub  30250
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 178  df-an 361
  Copyright terms: Public domain W3C validator