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  3875  iunxdif2  3966  exss  4252  xpiindi  4837  relssres  5008  nfunsn  5574  exfo  5694  fliftcnv  5826  f1oweALT  5867  fo1stres  6159  fo2ndres  6160  dftpos3  6268  tfrlem10  6419  odi  6593  omabs  6661  elixpsn  6871  sbthlem2  6988  sbthlem3  6989  fodomr  7028  mapxpen  7043  phplem2  7057  pssnn  7097  oieu  7270  inf3lem6  7350  acni3  7690  dfacacn  7783  kmlem1  7792  cflm  7892  cfsuc  7899  hsmexlem2  8069  hsmexlem4  8071  hsmexlem5  8072  axdc3lem4  8095  axcclem  8099  brdom5  8170  brdom4  8171  konigthlem  8206  alephval2  8210  alephmul  8216  reclem2pr  8688  suplem2pr  8693  lemulge11  9634  0mod  11011  1mod  11012  fzennn  11046  hashbclem  11406  resqrex  11752  demoivreALT  12497  pcdiv  12921  invsym2  13681  idghm  14714  gaid  14769  subrgid  15563  lbsextlem1  15927  mulgghm2  16475  topcld  16788  ntrss  16808  restcld  16919  xkocnv  17521  fbssfi  17548  isfild  17569  alexsublem  17754  alexsubALTlem4  17760  metrest  18086  dscopn  18112  reconnlem1  18347  cphsubrglem  18629  itgcnlem  19160  vieta1  19708  jensen  20299  nvge0  21256  ipval2  21296  sspg  21320  ssps  21322  sspmlem  21324  blocni  21399  ubthlem1  21465  bcsiALT  21774  ocsh  21878  chabs2  22112  pjoml6i  22184  osumcor2i  22239  nmopcoi  22691  opsqrlem6  22741  stlei  22836  mdslmd1lem1  22921  mdslmd2i  22926  atcvat3i  22992  atcvat4i  22993  sumdmdlem2  23015  dmdbr5ati  23018  ballotlemfp1  23066  ballotlemfmpn  23069  ballotlemsup  23079  xdivpnfrp  23133  prsiga  23507  faclimlem5  24121  wfr3g  24326  frr3g  24351  nodense  24414  nobndlem1  24417  nobnddown  24426  nofulllem3  24429  axlowdimlem6  24647  axlowdimlem7  24648  axlowdimlem16  24657  axlowdimlem17  24658  domfldrefc  25160  ranfldrefc  25161  domintrefb  25166  prl2  25272  istopx  25650  islimrs4  25685  trnij  25718  lvsovso  25729  propsrc  25971  trer  26330  fnessref  26396  refssfne  26397  filnetlem3  26432  filnetlem4  26433  prter1  26850  irrapx1  27016  dfacbasgrp  27376  dgraalem  27453  dgraaub  27456  dvsconst  27650  dvsid  27651  dvsef  27652  stoweidlem13  27865  stoweidlem17  27869  wallispilem1  27917  f1oun2prg  28187  s2f1o  28223  3v3e3cycl1  28390  4cycl4v4e  28412  4cycl4dv  28413  bnj545  29243  bnj548  29245  pmapsub  30579
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