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

Theorem jctil 539
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 534 1  |-  ( ph  ->  ( ch  /\  ps ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  jctl  543  nic-ax  1552  nic-axALT  1553  unidif  4255  iunxdif2  4350  exss  4685  xpiindi  4990  relssres  5162  nfunsn  5912  exfo  6055  fliftcnv  6219  f1oweALT  6791  fo1stres  6831  fo2ndres  6832  dftpos3  6999  wfr3g  7042  tfrlem10  7113  odi  7288  omabs  7356  elixpsn  7569  sbthlem2  7689  sbthlem3  7690  fodomr  7729  mapxpen  7744  phplem2  7758  pssnn  7796  oieu  8054  inf3lem6  8138  acni3  8476  dfacacn  8569  kmlem1  8578  cflm  8678  cfsuc  8685  hsmexlem2  8855  hsmexlem4  8857  hsmexlem5  8858  axdc3lem4  8881  axcclem  8885  brdom5  8955  brdom4  8956  konigthlem  8991  alephval2  8995  alephmul  9001  wunex3  9165  reclem2pr  9472  suplem2pr  9477  lemulge11  10466  nn0ge2m1nn  10934  0mod  12125  1mod  12126  fzennn  12178  hashbclem  12610  hash2prd  12627  hashge2el2dif  12630  wrdlenge2n0  12690  elovmptnn0wrd  12697  swrdnd  12773  2swrdeqwrdeq  12794  repswcshw  12896  s2f1o  12980  f1oun2prg  12981  cotrtrclfv  13055  resqrex  13293  demoivreALT  14233  pcdiv  14765  prmodvdslcmf  14968  prmordvdslcmfOLD  14982  invsym2  15619  idghm  16849  gaid  16904  subrgid  17945  lbsextlem1  18316  mulgghm2  18999  smadiadet  19626  pmatcollpw3fi  19740  topcld  19981  ntrss  20001  restcld  20119  xkocnv  20760  fbssfi  20783  isfild  20804  alexsublem  20990  alexsubALTlem4  20996  metrest  21470  dscopn  21519  reconnlem1  21755  cphsubrglem  22048  itgcnlem  22624  vieta1  23133  jensen  23779  axlowdimlem6  24823  axlowdimlem7  24824  axlowdimlem16  24833  axlowdimlem17  24834  cusgrafilem1  25052  0trlon  25123  2trllemE  25128  1pthon2v  25168  3v3e3cycl1  25217  4cycl4v4e  25239  4cycl4dv  25240  1conngra  25248  clwwlkf1  25369  usg2cwwkdifex  25394  rusgranumwlklem4  25525  rusgranumwwlkg  25532  numclwwlkovf2ex  25659  numclwwlkqhash  25673  nvge0  26148  ipval2  26188  sspg  26212  ssps  26214  sspmlem  26216  blocni  26291  ubthlem1  26357  bcsiALT  26667  ocsh  26771  chabs2  27005  pjoml6i  27077  osumcor2i  27132  nmopcoi  27583  opsqrlem6  27633  stlei  27728  mdslmd1lem1  27813  mdslmd2i  27818  atcvat3i  27884  atcvat4i  27885  sumdmdlem2  27907  dmdbr5ati  27910  xdivpnfrp  28240  oduprs  28255  tpr2rico  28557  ballotlemfp1  29150  ballotlemfc0  29151  ballotlemfcc  29152  ballotlemsup  29163  bnj545  29494  bnj548  29496  fv1stcnv  30209  fv2ndcnv  30210  frr3g  30300  nodense  30363  nobndlem1  30366  nobnddown  30375  nofulllem3  30378  trer  30757  filnetlem3  30821  filnetlem4  30822  phpreu  31632  poimirlem16  31659  poimirlem17  31660  poimirlem19  31662  poimirlem20  31663  poimirlem26  31669  mblfinlem1  31680  mblfinlem2  31681  mblfinlem3  31682  mblfinlem4  31683  ismblfin  31684  prter1  32158  pmapsub  33041  irrapx1  35381  dfacbasgrp  35672  dgraalem  35709  dgraaub  35712  dvsconst  36315  dvsid  36316  dvsef  36317  islptre  37270  wallispilem1  37495  fourierdlem52  37589  gbogt5  38252  gboage9  38254  nnsum3primesprm  38274  nnsum3primesgbe  38276  bgoldbnnsum3prm  38288  tgoldbachlt  38298  usgsizedg  38464  usgsizedgALT  38465  usgsizedgALT2  38466  lincext1  39006  linds0  39017  lindsrng01  39020  lmod1lem3  39041
  Copyright terms: Public domain W3C validator