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

Theorem jctil 521
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 513 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  jctl  525  nic-ax  1676  nic-axALT  1677  unidif  4907  iunxdif2  5017  exss  5424  xpiindi  5795  relssres  5982  frpoinsg  6301  nfunsn  6888  exfo  7059  fliftcnv  7260  oprres  7526  f1oweALT  7909  fo1stres  7951  fo2ndres  7952  dftpos3  8179  wfr3g  8257  tfrlem10  8337  odi  8530  omabs  8601  elixpsn  8881  sbthlem2  9034  sbthlem3  9035  fodomr  9078  mapxpen  9093  pssnn  9118  phplem2OLD  9168  pssnnOLD  9215  oieu  9483  inf3lem6  9577  frmin  9693  frr3g  9700  djuss  9864  acni3  9991  dfacacn  10085  kmlem1  10094  cflm  10194  cfsuc  10201  hsmexlem2  10371  hsmexlem4  10373  hsmexlem5  10374  axdc3lem4  10397  axcclem  10401  brdom5  10473  brdom4  10474  konigthlem  10512  alephval2  10516  alephmul  10522  wunex3  10685  reclem2pr  10992  suplem2pr  10997  lemulge11  12025  nn0ge2m1nn  12490  0mod  13816  1mod  13817  fzennn  13882  hashbclem  14358  hashge2el2dif  14388  wrdlenge2n0  14449  elovmptnn0wrd  14456  swrdnd  14551  s2f1o  14814  f1oun2prg  14815  cotrtrclfv  14906  resqrex  15144  modfsummods  15686  demoivreALT  16091  pcdiv  16732  prmodvdslcmf  16927  invsym2  17654  idghm  19031  gaid  19087  symgsubmefmndALT  19193  subrgid  20266  lbsextlem1  20664  mulgghm2  20920  smadiadet  22042  pmatcollpw3fi  22157  topcld  22409  ntrss  22429  restcld  22546  xkocnv  23188  fbssfi  23211  isfild  23232  alexsublem  23418  alexsubALTlem4  23424  metrest  23903  dscopn  23952  reconnlem1  24212  cphsubrglem  24564  cphipval  24630  itgcnlem  25177  vieta1  25695  jensen  26361  2lgs  26778  nosep1o  27052  nodense  27063  bdayimaon  27064  conway  27167  etasslt  27181  slerec  27187  cofcutr  27272  axlowdimlem6  27945  axlowdimlem7  27946  axlowdimlem16  27955  axlowdimlem17  27956  usgr2v1e2w  28249  0edg0rgr  28569  usgr2wlkspthlem2  28755  clwwlkf1  29042  0pthon  29120  ipval2  29698  sspg  29719  ssps  29721  sspmlem  29723  blocni  29796  ubthlem1  29861  bcsiALT  30170  ocsh  30274  chabs2  30508  pjoml6i  30580  osumcor2i  30635  nmopcoi  31086  opsqrlem6  31136  stlei  31231  mdslmd1lem1  31316  mdslmd2i  31321  atcvat3i  31387  atcvat4i  31388  sumdmdlem2  31410  dmdbr5ati  31413  xdivpnfrp  31845  oduprs  31880  tpr2rico  32557  ballotlemfp1  33155  ballotlemfc0  33156  ballotlemfcc  33157  ballotlemsup  33168  tgoldbachgt  33340  bnj545  33571  bnj548  33573  satfv1  34021  trer  34841  filnetlem3  34905  filnetlem4  34906  phpreu  36112  matunitlindflem1  36124  poimirlem16  36144  poimirlem17  36145  poimirlem19  36147  poimirlem20  36148  poimirlem26  36154  mblfinlem1  36165  mblfinlem2  36166  mblfinlem3  36167  mblfinlem4  36168  ismblfin  36169  prter1  37391  pmapsub  38281  2xp3dxp2ge1d  40664  irrapx1  41198  dfacbasgrp  41482  dgraalem  41519  dgraaub  41522  onexlimgt  41624  cantnftermord  41702  oacl2g  41712  onmcl  41713  omabs2  41714  omcl2  41715  ofoaf  41718  naddwordnexlem3  41763  naddwordnexlem4  41765  brcoffn  42394  clsk3nimkb  42404  clsk1indlem1  42409  dvsconst  42702  dvsid  42703  dvsef  42704  islptre  43950  wallispilem1  44396  fourierdlem52  44489  ovnhoilem1  44932  gbowgt5  46044  gboge9  46046  nnsum3primesprm  46072  nnsum3primesgbe  46074  bgoldbnnsum3prm  46086  tgoldbachlt  46098  lincext1  46625  linds0  46636  lindsrng01  46639  lmod1lem3  46660  line2  46928  line2x  46930  inlinecirc02plem  46962  setrec1  47226
  Copyright terms: Public domain W3C validator