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

Theorem jctil 534
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 529 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  538  nic-ax  1485  nic-axALT  1486  unidif  4122  iunxdif2  4215  exss  4552  xpiindi  4971  relssres  5144  nfunsn  5718  exfo  5858  fliftcnv  6001  f1oweALT  6560  fo1stres  6599  fo2ndres  6600  dftpos3  6762  tfrlem10  6842  odi  7014  omabs  7082  elixpsn  7298  sbthlem2  7418  sbthlem3  7419  fodomr  7458  mapxpen  7473  phplem2  7487  pssnn  7527  oieu  7749  inf3lem6  7835  acni3  8213  dfacacn  8306  kmlem1  8315  cflm  8415  cfsuc  8422  hsmexlem2  8592  hsmexlem4  8594  hsmexlem5  8595  axdc3lem4  8618  axcclem  8622  brdom5  8692  brdom4  8693  konigthlem  8728  alephval2  8732  alephmul  8738  wunex3  8904  reclem2pr  9213  suplem2pr  9218  lemulge11  10187  0mod  11735  1mod  11736  fzennn  11786  hash2prd  12177  hashge2el2dif  12180  hashbclem  12201  wrdlenge2n0  12257  swrdlend  12321  swrd0  12323  2swrdeqwrdeq  12343  repswcshw  12442  s2f1o  12522  f1oun2prg  12523  resqrex  12736  demoivreALT  13481  pcdiv  13915  invsym2  14697  idghm  15755  gaid  15810  subrgid  16847  lbsextlem1  17217  mulgghm2  17884  mulgghm2OLD  17887  smadiadet  18435  topcld  18598  ntrss  18618  restcld  18735  xkocnv  19346  fbssfi  19369  isfild  19390  alexsublem  19575  alexsubALTlem4  19581  metrest  20058  dscopn  20125  reconnlem1  20362  cphsubrglem  20655  itgcnlem  21226  vieta1  21737  jensen  22341  axlowdimlem6  23128  axlowdimlem7  23129  axlowdimlem16  23138  axlowdimlem17  23139  cusgrafilem1  23322  0trlon  23382  2trllemE  23387  1pthon2v  23427  3v3e3cycl1  23465  4cycl4v4e  23487  4cycl4dv  23488  1conngra  23496  nvge0  23997  ipval2  24037  sspg  24061  ssps  24063  sspmlem  24065  blocni  24140  ubthlem1  24206  bcsiALT  24516  ocsh  24621  chabs2  24855  pjoml6i  24927  osumcor2i  24982  nmopcoi  25434  opsqrlem6  25484  stlei  25579  mdslmd1lem1  25664  mdslmd2i  25669  atcvat3i  25735  atcvat4i  25736  sumdmdlem2  25758  dmdbr5ati  25761  xdivpnfrp  26041  tpr2rico  26278  ballotlemfp1  26804  ballotlemfc0  26805  ballotlemfcc  26806  ballotlemsup  26817  wfr3g  27652  frr3g  27696  nodense  27759  nobndlem1  27762  nobnddown  27771  nofulllem3  27774  mblfinlem1  28353  mblfinlem2  28354  mblfinlem3  28355  mblfinlem4  28356  ismblfin  28357  trer  28436  fnessref  28490  refssfne  28491  filnetlem3  28526  filnetlem4  28527  prter1  28949  irrapx1  29094  dfacbasgrp  29389  dgraalem  29427  dgraaub  29430  areaquad  29517  dvsconst  29529  dvsid  29530  dvsef  29531  wallispilem1  29785  elovmptnn0wrd  30182  clwwlkf1  30383  usg2cwwkdifex  30420  rusgranumwlklem4  30495  rusgranumwwlkg  30502  numclwwlkovf2ex  30604  numclwwlkqhash  30618  lincext1  30829  linds0  30840  lindsrng01  30843  lmod1lem3  30872  bnj545  31722  bnj548  31724  pmapsub  33134
  Copyright terms: Public domain W3C validator