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

Theorem jctil 559
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 553 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 385
This theorem is referenced by:  jctl  563  nic-ax  1638  nic-axALT  1639  unidif  4503  iunxdif2  4600  exss  4961  xpiindi  5290  relssres  5472  nfunsn  6263  exfo  6417  fliftcnv  6601  oprres  6844  f1oweALT  7194  fo1stres  7236  fo2ndres  7237  dftpos3  7415  wfr3g  7458  tfrlem10  7528  odi  7704  omabs  7772  elixpsn  7989  sbthlem2  8112  sbthlem3  8113  fodomr  8152  mapxpen  8167  phplem2  8181  pssnn  8219  oieu  8485  inf3lem6  8568  acni3  8908  dfacacn  9001  kmlem1  9010  cflm  9110  cfsuc  9117  hsmexlem2  9287  hsmexlem4  9289  hsmexlem5  9290  axdc3lem4  9313  axcclem  9317  brdom5  9389  brdom4  9390  konigthlem  9428  alephval2  9432  alephmul  9438  wunex3  9601  reclem2pr  9908  suplem2pr  9913  lemulge11  10923  nn0ge2m1nn  11398  0mod  12741  1mod  12742  fzennn  12807  hashbclem  13274  hashge2el2dif  13300  wrdlenge2n0  13374  elovmptnn0wrd  13381  swrdnd  13478  2swrdeqwrdeq  13499  repswcshw  13604  s2f1o  13707  f1oun2prg  13708  cotrtrclfv  13797  resqrex  14035  modfsummods  14569  demoivreALT  14975  pcdiv  15604  prmodvdslcmf  15798  invsym2  16470  idghm  17722  gaid  17778  subrgid  18830  lbsextlem1  19206  mulgghm2  19893  smadiadet  20524  pmatcollpw3fi  20638  topcld  20887  ntrss  20907  restcld  21024  xkocnv  21665  fbssfi  21688  isfild  21709  alexsublem  21895  alexsubALTlem4  21901  metrest  22376  dscopn  22425  reconnlem1  22676  cphsubrglem  23023  cphipval  23088  itgcnlem  23601  vieta1  24112  jensen  24760  2lgs  25177  axlowdimlem6  25872  axlowdimlem7  25873  axlowdimlem16  25882  axlowdimlem17  25883  usgr2v1e2w  26189  0edg0rgr  26524  usgr2wlkspthlem2  26710  clwwlkf1  27012  0pthon  27105  nvge0  27656  ipval2  27690  sspg  27711  ssps  27713  sspmlem  27715  blocni  27788  ubthlem1  27854  bcsiALT  28164  ocsh  28270  chabs2  28504  pjoml6i  28576  osumcor2i  28631  nmopcoi  29082  opsqrlem6  29132  stlei  29227  mdslmd1lem1  29312  mdslmd2i  29317  atcvat3i  29383  atcvat4i  29384  sumdmdlem2  29406  dmdbr5ati  29409  xdivpnfrp  29769  oduprs  29784  tpr2rico  30086  ballotlemfp1  30681  ballotlemfc0  30682  ballotlemfcc  30683  ballotlemsup  30694  tgoldbachgt  30869  bnj545  31091  bnj548  31093  fv1stcnv  31804  fv2ndcnv  31805  frpoinsg  31866  frr3g  31904  nosep1o  31957  nodense  31967  bdayimaon  31968  nulsslt  32033  conway  32035  etasslt  32045  slerec  32048  trer  32435  filnetlem3  32500  filnetlem4  32501  phpreu  33523  matunitlindflem1  33535  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem26  33565  mblfinlem1  33576  mblfinlem2  33577  mblfinlem3  33578  mblfinlem4  33579  ismblfin  33580  prter1  34483  pmapsub  35372  irrapx1  37709  dfacbasgrp  37995  dgraalem  38032  dgraaub  38035  brcoffn  38645  clsk3nimkb  38655  clsk1indlem1  38660  dvsconst  38846  dvsid  38847  dvsef  38848  islptre  40169  wallispilem1  40600  fourierdlem52  40693  ovnhoilem1  41136  gbowgt5  41975  gboge9  41977  nnsum3primesprm  42003  nnsum3primesgbe  42005  bgoldbnnsum3prm  42017  tgoldbachlt  42029  tgoldbachltOLD  42035  lincext1  42568  linds0  42579  lindsrng01  42582  lmod1lem3  42603  setrec1  42763
  Copyright terms: Public domain W3C validator