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  1490  nic-axALT  1491  unidif  4279  iunxdif2  4373  exss  4710  xpiindi  5136  relssres  5309  nfunsn  5895  exfo  6037  fliftcnv  6195  f1oweALT  6765  fo1stres  6805  fo2ndres  6806  dftpos3  6970  tfrlem10  7053  odi  7225  omabs  7293  elixpsn  7505  sbthlem2  7625  sbthlem3  7626  fodomr  7665  mapxpen  7680  phplem2  7694  pssnn  7735  oieu  7960  inf3lem6  8046  acni3  8424  dfacacn  8517  kmlem1  8526  cflm  8626  cfsuc  8633  hsmexlem2  8803  hsmexlem4  8805  hsmexlem5  8806  axdc3lem4  8829  axcclem  8833  brdom5  8903  brdom4  8904  konigthlem  8939  alephval2  8943  alephmul  8949  wunex3  9115  reclem2pr  9422  suplem2pr  9427  lemulge11  10400  0mod  11991  1mod  11992  fzennn  12042  hashbclem  12463  hash2prd  12480  hashge2el2dif  12483  wrdlenge2n0  12538  elovmptnn0wrd  12545  swrdlend  12615  swrd0  12617  2swrdeqwrdeq  12637  repswcshw  12739  s2f1o  12823  f1oun2prg  12824  resqrex  13043  demoivreALT  13793  pcdiv  14231  invsym2  15014  idghm  16077  gaid  16132  subrgid  17214  lbsextlem1  17587  mulgghm2  18298  mulgghm2OLD  18301  smadiadet  18939  pmatcollpw3fi  19053  topcld  19302  ntrss  19322  restcld  19439  xkocnv  20050  fbssfi  20073  isfild  20094  alexsublem  20279  alexsubALTlem4  20285  metrest  20762  dscopn  20829  reconnlem1  21066  cphsubrglem  21359  itgcnlem  21931  vieta1  22442  jensen  23046  axlowdimlem6  23926  axlowdimlem7  23927  axlowdimlem16  23936  axlowdimlem17  23937  cusgrafilem1  24155  0trlon  24226  2trllemE  24231  1pthon2v  24271  3v3e3cycl1  24320  4cycl4v4e  24342  4cycl4dv  24343  1conngra  24351  clwwlkf1  24472  usg2cwwkdifex  24497  rusgranumwlklem4  24628  rusgranumwwlkg  24635  numclwwlkovf2ex  24763  numclwwlkqhash  24777  nvge0  25253  ipval2  25293  sspg  25317  ssps  25319  sspmlem  25321  blocni  25396  ubthlem1  25462  bcsiALT  25772  ocsh  25877  chabs2  26111  pjoml6i  26183  osumcor2i  26238  nmopcoi  26690  opsqrlem6  26740  stlei  26835  mdslmd1lem1  26920  mdslmd2i  26925  atcvat3i  26991  atcvat4i  26992  sumdmdlem2  27014  dmdbr5ati  27017  xdivpnfrp  27297  tpr2rico  27530  ballotlemfp1  28070  ballotlemfc0  28071  ballotlemfcc  28072  ballotlemsup  28083  wfr3g  28919  frr3g  28963  nodense  29026  nobndlem1  29029  nobnddown  29038  nofulllem3  29041  mblfinlem1  29628  mblfinlem2  29629  mblfinlem3  29630  mblfinlem4  29631  ismblfin  29632  trer  29711  fnessref  29765  refssfne  29766  filnetlem3  29801  filnetlem4  29802  prter1  30224  irrapx1  30368  dfacbasgrp  30661  dgraalem  30699  dgraaub  30702  dvsconst  30835  dvsid  30836  dvsef  30837  wallispilem1  31365  usgsizedg  31864  usgsizedgALT  31865  usgsizedgALT2  31866  lincext1  32128  linds0  32139  lindsrng01  32142  lmod1lem3  32171  bnj545  33032  bnj548  33034  pmapsub  34564
  Copyright terms: Public domain W3C validator