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

Theorem jctil 524
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 519 1  |-  ( ph  ->  ( ch  /\  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  jctl  526  nic-ax  1447  nic-axALT  1448  unidif  4039  iunxdif2  4131  exss  4418  xpiindi  5002  relssres  5175  nfunsn  5753  exfo  5879  fliftcnv  6025  f1oweALT  6066  fo1stres  6362  fo2ndres  6363  dftpos3  6489  tfrlem10  6640  odi  6814  omabs  6882  elixpsn  7093  sbthlem2  7210  sbthlem3  7211  fodomr  7250  mapxpen  7265  phplem2  7279  pssnn  7319  oieu  7500  inf3lem6  7580  acni3  7920  dfacacn  8013  kmlem1  8022  cflm  8122  cfsuc  8129  hsmexlem2  8299  hsmexlem4  8301  hsmexlem5  8302  axdc3lem4  8325  axcclem  8329  brdom5  8399  brdom4  8400  konigthlem  8435  alephval2  8439  alephmul  8445  wunex3  8608  reclem2pr  8917  suplem2pr  8922  lemulge11  9864  0mod  11264  1mod  11265  fzennn  11299  hashbclem  11693  s2f1o  11855  f1oun2prg  11856  resqrex  12048  demoivreALT  12794  pcdiv  13218  invsym2  13980  idghm  15013  gaid  15068  subrgid  15862  lbsextlem1  16222  mulgghm2  16778  topcld  17091  ntrss  17111  restcld  17228  xkocnv  17838  fbssfi  17861  isfild  17882  alexsublem  18067  alexsubALTlem4  18073  metrest  18546  dscopn  18613  reconnlem1  18849  cphsubrglem  19132  itgcnlem  19673  vieta1  20221  jensen  20819  cusgrafilem1  21480  0trlon  21540  2trllemE  21545  1pthon2v  21585  3v3e3cycl1  21623  4cycl4v4e  21645  4cycl4dv  21646  1conngra  21654  nvge0  22155  ipval2  22195  sspg  22219  ssps  22221  sspmlem  22223  blocni  22298  ubthlem1  22364  bcsiALT  22673  ocsh  22777  chabs2  23011  pjoml6i  23083  osumcor2i  23138  nmopcoi  23590  opsqrlem6  23640  stlei  23735  mdslmd1lem1  23820  mdslmd2i  23825  atcvat3i  23891  atcvat4i  23892  sumdmdlem2  23914  dmdbr5ati  23917  xdivpnfrp  24171  tpr2rico  24302  ballotlemfp1  24741  ballotlemfc0  24742  ballotlemfcc  24743  ballotlemsup  24754  wfr3g  25529  frr3g  25573  nodense  25636  nobndlem1  25639  nobnddown  25648  nofulllem3  25651  axlowdimlem6  25878  axlowdimlem7  25879  axlowdimlem16  25888  axlowdimlem17  25889  mblfinlem  26234  mblfinlem2  26235  mblfinlem3  26236  ismblfin  26237  trer  26310  fnessref  26364  refssfne  26365  filnetlem3  26400  filnetlem4  26401  prter1  26719  irrapx1  26882  dfacbasgrp  27241  dgraalem  27318  dgraaub  27321  dvsconst  27515  dvsid  27516  dvsef  27517  wallispilem1  27781  swrdltnd  28153  bnj545  29203  bnj548  29205  pmapsub  30502
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 178  df-an 361
  Copyright terms: Public domain W3C validator