Theorem jctil 560

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

Step	Hyp	Ref	Expression
1		jctil.2	. . 3 |- ch
2	1	a1i 11	. 2 |- ( ph -> ch )
3		jctil.1	. 2 |- ( ph -> ps )
4	2, 3	jca 554	1 |- ( ph -> ( ch /\ ps ) )

Syntax hints:   -> wi 4   /\ wa 384

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 197  df-an 386

This theorem is referenced by:  jctl  564  nic-ax  1598  nic-axALT  1599  unidif  4471  iunxdif2  4568  exss  4931  xpiindi  5257  relssres  5437  nfunsn  6225  exfo  6377  fliftcnv  6561  oprres  6802  f1oweALT  7152  fo1stres  7192  fo2ndres  7193  dftpos3  7370  wfr3g  7413  tfrlem10  7483  odi  7659  omabs  7727  elixpsn  7947  sbthlem2  8071  sbthlem3  8072  fodomr  8111  mapxpen  8126  phplem2  8140  pssnn  8178  oieu  8444  inf3lem6  8530  acni3  8870  dfacacn  8963  kmlem1  8972  cflm  9072  cfsuc  9079  hsmexlem2  9249  hsmexlem4  9251  hsmexlem5  9252  axdc3lem4  9275  axcclem  9279  brdom5  9351  brdom4  9352  konigthlem  9390  alephval2  9394  alephmul  9400  wunex3  9563  reclem2pr  9870  suplem2pr  9875  lemulge11  10885  nn0ge2m1nn  11360  0mod  12701  1mod  12702  fzennn  12767  hashbclem  13236  hashge2el2dif  13262  wrdlenge2n0  13341  elovmptnn0wrd  13348  swrdnd  13432  2swrdeqwrdeq  13453  repswcshw  13558  s2f1o  13661  f1oun2prg  13662  cotrtrclfv  13753  resqrex  13991  modfsummods  14525  demoivreALT  14931  pcdiv  15557  prmodvdslcmf  15751  invsym2  16423  idghm  17675  gaid  17732  subrgid  18782  lbsextlem1  19158  mulgghm2  19845  smadiadet  20476  pmatcollpw3fi  20590  topcld  20839  ntrss  20859  restcld  20976  xkocnv  21617  fbssfi  21641  isfild  21662  alexsublem  21848  alexsubALTlem4  21854  metrest  22329  dscopn  22378  reconnlem1  22629  cphsubrglem  22977  cphipval  23042  itgcnlem  23556  vieta1  24067  jensen  24715  2lgs  25132  axlowdimlem6  25827  axlowdimlem7  25828  axlowdimlem16  25837  axlowdimlem17  25838  usgr2v1e2w  26144  0edg0rgr  26468  usgr2wlkspthlem2  26654  clwwlksf1  26917  0pthon  26988  nvge0  27528  ipval2  27562  sspg  27583  ssps  27585  sspmlem  27587  blocni  27660  ubthlem1  27726  bcsiALT  28036  ocsh  28142  chabs2  28376  pjoml6i  28448  osumcor2i  28503  nmopcoi  28954  opsqrlem6  29004  stlei  29099  mdslmd1lem1  29184  mdslmd2i  29189  atcvat3i  29255  atcvat4i  29256  sumdmdlem2  29278  dmdbr5ati  29281  xdivpnfrp  29641  oduprs  29656  tpr2rico  29958  ballotlemfp1  30553  ballotlemfc0  30554  ballotlemfcc  30555  ballotlemsup  30566  tgoldbachgt  30741  bnj545  30965  bnj548  30967  fv1stcnv  31680  fv2ndcnv  31681  frr3g  31779  nosep1o  31832  nodense  31842  bdayimaon  31843  nulsslt  31908  conway  31910  etasslt  31920  slerec  31923  trer  32310  filnetlem3  32375  filnetlem4  32376  phpreu  33393  matunitlindflem1  33405  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem26  33435  mblfinlem1  33446  mblfinlem2  33447  mblfinlem3  33448  mblfinlem4  33449  ismblfin  33450  prter1  34164  pmapsub  35054  irrapx1  37392  dfacbasgrp  37678  dgraalem  37715  dgraaub  37718  brcoffn  38328  clsk3nimkb  38338  clsk1indlem1  38343  dvsconst  38529  dvsid  38530  dvsef  38531  islptre  39851  wallispilem1  40282  fourierdlem52  40375  ovnhoilem1  40815  gbowgt5  41650  gboge9  41652  nnsum3primesprm  41678  nnsum3primesgbe  41680  bgoldbnnsum3prm  41692  tgoldbachlt  41704  tgoldbachltOLD  41710  lincext1  42243  linds0  42254  lindsrng01  42257  lmod1lem3  42278  setrec1  42438