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

Theorem jctil 509
Description: Inference conjoining a theorem to left of consequent in an implication. (Contributed by NM, 31-Dec-1993.)
Hypotheses
Ref Expression
jctil.1 (𝜑𝜓)
jctil.2 𝜒
Assertion
Ref Expression
jctil (𝜑 → (𝜒𝜓))

Proof of Theorem jctil
StepHypRef Expression
1 jctil.2 . . 3 𝜒
21a1i 11 . 2 (𝜑𝜒)
3 jctil.1 . 2 (𝜑𝜓)
42, 3jca 501 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 383
This theorem is referenced by:  jctl  513  nic-ax  1746  nic-axALT  1747  unidif  4607  iunxdif2  4702  exss  5059  xpiindi  5396  relssres  5578  nfunsn  6366  exfo  6520  fliftcnv  6704  oprres  6949  f1oweALT  7299  fo1stres  7341  fo2ndres  7342  dftpos3  7522  wfr3g  7565  tfrlem10  7636  odi  7813  omabs  7881  elixpsn  8101  sbthlem2  8227  sbthlem3  8228  fodomr  8267  mapxpen  8282  phplem2  8296  pssnn  8334  oieu  8600  inf3lem6  8694  djuss  8946  acni3  9070  dfacacn  9165  kmlem1  9174  cflm  9274  cfsuc  9281  hsmexlem2  9451  hsmexlem4  9453  hsmexlem5  9454  axdc3lem4  9477  axcclem  9481  brdom5  9553  brdom4  9554  konigthlem  9592  alephval2  9596  alephmul  9602  wunex3  9765  reclem2pr  10072  suplem2pr  10077  lemulge11  11087  nn0ge2m1nn  11562  0mod  12909  1mod  12910  fzennn  12975  hashbclem  13438  hashge2el2dif  13464  wrdlenge2n0  13538  elovmptnn0wrd  13545  swrdnd  13641  2swrdeqwrdeq  13662  repswcshw  13767  s2f1o  13870  f1oun2prg  13871  cotrtrclfv  13961  resqrex  14199  modfsummods  14732  demoivreALT  15137  pcdiv  15764  prmodvdslcmf  15958  invsym2  16630  idghm  17883  gaid  17939  subrgid  18992  lbsextlem1  19373  mulgghm2  20060  smadiadet  20695  pmatcollpw3fi  20810  topcld  21060  ntrss  21080  restcld  21197  xkocnv  21838  fbssfi  21861  isfild  21882  alexsublem  22068  alexsubALTlem4  22074  metrest  22549  dscopn  22598  reconnlem1  22849  cphsubrglem  23196  cphipval  23261  itgcnlem  23776  vieta1  24287  jensen  24936  2lgs  25353  axlowdimlem6  26048  axlowdimlem7  26049  axlowdimlem16  26058  axlowdimlem17  26059  usgr2v1e2w  26367  0edg0rgr  26703  usgr2wlkspthlem2  26889  clwwlkf1  27205  0pthon  27307  ipval2  27902  sspg  27923  ssps  27925  sspmlem  27927  blocni  28000  ubthlem1  28066  bcsiALT  28376  ocsh  28482  chabs2  28716  pjoml6i  28788  osumcor2i  28843  nmopcoi  29294  opsqrlem6  29344  stlei  29439  mdslmd1lem1  29524  mdslmd2i  29529  atcvat3i  29595  atcvat4i  29596  sumdmdlem2  29618  dmdbr5ati  29621  xdivpnfrp  29981  oduprs  29996  tpr2rico  30298  ballotlemfp1  30893  ballotlemfc0  30894  ballotlemfcc  30895  ballotlemsup  30906  tgoldbachgt  31081  bnj545  31303  bnj548  31305  fv1stcnv  32016  fv2ndcnv  32017  frpoinsg  32078  frr3g  32116  nosep1o  32169  nodense  32179  bdayimaon  32180  nulsslt  32245  conway  32247  etasslt  32257  slerec  32260  trer  32647  filnetlem3  32712  filnetlem4  32713  phpreu  33726  matunitlindflem1  33738  poimirlem16  33758  poimirlem17  33759  poimirlem19  33761  poimirlem20  33762  poimirlem26  33768  mblfinlem1  33779  mblfinlem2  33780  mblfinlem3  33781  mblfinlem4  33782  ismblfin  33783  prter1  34687  pmapsub  35576  irrapx1  37918  dfacbasgrp  38204  dgraalem  38241  dgraaub  38244  brcoffn  38854  clsk3nimkb  38864  clsk1indlem1  38869  dvsconst  39055  dvsid  39056  dvsef  39057  islptre  40369  wallispilem1  40799  fourierdlem52  40892  ovnhoilem1  41335  gbowgt5  42178  gboge9  42180  nnsum3primesprm  42206  nnsum3primesgbe  42208  bgoldbnnsum3prm  42220  tgoldbachlt  42232  tgoldbachltOLD  42238  lincext1  42771  linds0  42782  lindsrng01  42785  lmod1lem3  42806  setrec1  42966
  Copyright terms: Public domain W3C validator