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

Theorem jctil 525
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 520 1  |-  ( ph  ->  ( ch  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 360
This theorem is referenced by:  jctl  527  nic-ax  1448  nic-axALT  1449  unidif  4049  iunxdif2  4141  exss  4429  xpiindi  5013  relssres  5186  nfunsn  5764  exfo  5890  fliftcnv  6036  f1oweALT  6077  fo1stres  6373  fo2ndres  6374  dftpos3  6500  tfrlem10  6651  odi  6825  omabs  6893  elixpsn  7104  sbthlem2  7221  sbthlem3  7222  fodomr  7261  mapxpen  7276  phplem2  7290  pssnn  7330  oieu  7511  inf3lem6  7591  acni3  7933  dfacacn  8026  kmlem1  8035  cflm  8135  cfsuc  8142  hsmexlem2  8312  hsmexlem4  8314  hsmexlem5  8315  axdc3lem4  8338  axcclem  8342  brdom5  8412  brdom4  8413  konigthlem  8448  alephval2  8452  alephmul  8458  wunex3  8621  reclem2pr  8930  suplem2pr  8935  lemulge11  9877  0mod  11277  1mod  11278  fzennn  11312  hashbclem  11706  s2f1o  11868  f1oun2prg  11869  resqrex  12061  demoivreALT  12807  pcdiv  13231  invsym2  13993  idghm  15026  gaid  15081  subrgid  15875  lbsextlem1  16235  mulgghm2  16791  topcld  17104  ntrss  17124  restcld  17241  xkocnv  17851  fbssfi  17874  isfild  17895  alexsublem  18080  alexsubALTlem4  18086  metrest  18559  dscopn  18626  reconnlem1  18862  cphsubrglem  19145  itgcnlem  19684  vieta1  20234  jensen  20832  cusgrafilem1  21493  0trlon  21553  2trllemE  21558  1pthon2v  21598  3v3e3cycl1  21636  4cycl4v4e  21658  4cycl4dv  21659  1conngra  21667  nvge0  22168  ipval2  22208  sspg  22232  ssps  22234  sspmlem  22236  blocni  22311  ubthlem1  22377  bcsiALT  22686  ocsh  22790  chabs2  23024  pjoml6i  23096  osumcor2i  23151  nmopcoi  23603  opsqrlem6  23653  stlei  23748  mdslmd1lem1  23833  mdslmd2i  23838  atcvat3i  23904  atcvat4i  23905  sumdmdlem2  23927  dmdbr5ati  23930  xdivpnfrp  24184  tpr2rico  24315  ballotlemfp1  24754  ballotlemfc0  24755  ballotlemfcc  24756  ballotlemsup  24767  wfr3g  25542  frr3g  25586  nodense  25649  nobndlem1  25652  nobnddown  25661  nofulllem3  25664  axlowdimlem6  25891  axlowdimlem7  25892  axlowdimlem16  25901  axlowdimlem17  25902  mblfinlem1  26255  mblfinlem2  26256  mblfinlem3  26257  mblfinlem4  26258  ismblfin  26259  trer  26333  fnessref  26387  refssfne  26388  filnetlem3  26423  filnetlem4  26424  prter1  26742  irrapx1  26905  dfacbasgrp  27264  dgraalem  27341  dgraaub  27344  dvsconst  27538  dvsid  27539  dvsef  27540  wallispilem1  27804  swrdltnd  28215  bnj545  29340  bnj548  29342  pmapsub  30639
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 179  df-an 362
  Copyright terms: Public domain W3C validator