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

Theorem jctil 523
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 10 . 2  |-  ( ph  ->  ch )
3 jctil.1 . 2  |-  ( ph  ->  ps )
42, 3jca 518 1  |-  ( ph  ->  ( ch  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  jctl  525  nic-ax  1428  nic-axALT  1429  unidif  3859  iunxdif2  3950  exss  4236  xpiindi  4821  relssres  4992  nfunsn  5558  exfo  5678  fliftcnv  5810  f1oweALT  5851  fo1stres  6143  fo2ndres  6144  dftpos3  6252  tfrlem10  6403  odi  6577  omabs  6645  elixpsn  6855  sbthlem2  6972  sbthlem3  6973  fodomr  7012  mapxpen  7027  phplem2  7041  pssnn  7081  oieu  7254  inf3lem6  7334  acni3  7674  dfacacn  7767  kmlem1  7776  cflm  7876  cfsuc  7883  hsmexlem2  8053  hsmexlem4  8055  hsmexlem5  8056  axdc3lem4  8079  axcclem  8083  brdom5  8154  brdom4  8155  konigthlem  8190  alephval2  8194  alephmul  8200  reclem2pr  8672  suplem2pr  8677  lemulge11  9618  0mod  10995  1mod  10996  fzennn  11030  hashbclem  11390  resqrex  11736  demoivreALT  12481  pcdiv  12905  invsym2  13665  idghm  14698  gaid  14753  subrgid  15547  lbsextlem1  15911  mulgghm2  16459  topcld  16772  ntrss  16792  restcld  16903  xkocnv  17505  fbssfi  17532  isfild  17553  alexsublem  17738  alexsubALTlem4  17744  metrest  18070  dscopn  18096  reconnlem1  18331  cphsubrglem  18613  itgcnlem  19144  vieta1  19692  jensen  20283  nvge0  21240  ipval2  21280  sspg  21304  ssps  21306  sspmlem  21308  blocni  21383  ubthlem1  21449  bcsiALT  21758  ocsh  21862  chabs2  22096  pjoml6i  22168  osumcor2i  22223  nmopcoi  22675  opsqrlem6  22725  stlei  22820  mdslmd1lem1  22905  mdslmd2i  22910  atcvat3i  22976  atcvat4i  22977  sumdmdlem2  22999  dmdbr5ati  23002  ballotlemfp1  23050  ballotlemfmpn  23053  ballotlemsup  23063  xdivpnfrp  23117  prsiga  23492  wfr3g  24255  frr3g  24280  nodense  24343  nobndlem1  24346  nobnddown  24355  nofulllem3  24358  axlowdimlem6  24575  axlowdimlem7  24576  axlowdimlem16  24585  axlowdimlem17  24586  domfldrefc  25057  ranfldrefc  25058  domintrefb  25063  prl2  25169  istopx  25547  islimrs4  25582  trnij  25615  lvsovso  25626  propsrc  25868  trer  26227  fnessref  26293  refssfne  26294  filnetlem3  26329  filnetlem4  26330  prter1  26747  irrapx1  26913  dfacbasgrp  27273  dgraalem  27350  dgraaub  27353  dvsconst  27547  dvsid  27548  dvsef  27549  stoweidlem13  27762  stoweidlem17  27766  wallispilem1  27814  f1oun2prg  28076  s2f1o  28091  bnj545  28927  bnj548  28929  pmapsub  29957
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 177  df-an 360
  Copyright terms: Public domain W3C validator