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

Theorem jctil 523
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 515 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  jctl  527  nic-ax  1675  nic-axALT  1676  unidif  4858  iunxdif2  4963  exss  5343  xpiindi  5694  relssres  5882  nfunsn  6700  exfo  6864  fliftcnv  7059  oprres  7312  f1oweALT  7670  fo1stres  7712  fo2ndres  7713  dftpos3  7908  wfr3g  7951  tfrlem10  8021  odi  8203  omabs  8272  elixpsn  8499  sbthlem2  8627  sbthlem3  8628  fodomr  8667  mapxpen  8682  phplem2  8696  pssnn  8735  oieu  9002  inf3lem6  9095  djuss  9348  acni3  9473  dfacacn  9567  kmlem1  9576  cflm  9672  cfsuc  9679  hsmexlem2  9849  hsmexlem4  9851  hsmexlem5  9852  axdc3lem4  9875  axcclem  9879  brdom5  9951  brdom4  9952  konigthlem  9990  alephval2  9994  alephmul  10000  wunex3  10163  reclem2pr  10470  suplem2pr  10475  lemulge11  11502  nn0ge2m1nn  11963  0mod  13276  1mod  13277  fzennn  13342  hashbclem  13817  hashge2el2dif  13845  wrdlenge2n0  13906  elovmptnn0wrd  13913  swrdnd  14018  s2f1o  14280  f1oun2prg  14281  cotrtrclfv  14374  resqrex  14612  modfsummods  15150  demoivreALT  15556  pcdiv  16189  prmodvdslcmf  16383  invsym2  17035  idghm  18375  gaid  18431  symgsubmefmndALT  18533  subrgid  19539  lbsextlem1  19932  mulgghm2  20199  smadiadet  21284  pmatcollpw3fi  21399  topcld  21649  ntrss  21669  restcld  21786  xkocnv  22428  fbssfi  22451  isfild  22472  alexsublem  22658  alexsubALTlem4  22664  metrest  23140  dscopn  23189  reconnlem1  23440  cphsubrglem  23791  cphipval  23856  itgcnlem  24402  vieta1  24917  jensen  25583  2lgs  26000  axlowdimlem6  26750  axlowdimlem7  26751  axlowdimlem16  26760  axlowdimlem17  26761  usgr2v1e2w  27051  0edg0rgr  27371  usgr2wlkspthlem2  27556  clwwlkf1  27843  0pthon  27921  ipval2  28499  sspg  28520  ssps  28522  sspmlem  28524  blocni  28597  ubthlem1  28662  bcsiALT  28971  ocsh  29075  chabs2  29309  pjoml6i  29381  osumcor2i  29436  nmopcoi  29887  opsqrlem6  29937  stlei  30032  mdslmd1lem1  30117  mdslmd2i  30122  atcvat3i  30188  atcvat4i  30189  sumdmdlem2  30211  dmdbr5ati  30214  xdivpnfrp  30630  oduprs  30664  tpr2rico  31240  ballotlemfp1  31834  ballotlemfc0  31835  ballotlemfcc  31836  ballotlemsup  31847  tgoldbachgt  32019  bnj545  32252  bnj548  32254  satfv1  32695  frpoinsg  33166  frr3g  33206  nosep1o  33271  nodense  33281  bdayimaon  33282  nulsslt  33347  conway  33349  etasslt  33359  slerec  33362  trer  33749  filnetlem3  33813  filnetlem4  33814  phpreu  35013  matunitlindflem1  35025  poimirlem16  35045  poimirlem17  35046  poimirlem19  35048  poimirlem20  35049  poimirlem26  35055  mblfinlem1  35066  mblfinlem2  35067  mblfinlem3  35068  mblfinlem4  35069  ismblfin  35070  prter1  36147  pmapsub  37036  2xp3dxp2ge1d  39351  irrapx1  39713  dfacbasgrp  39996  dgraalem  40033  dgraaub  40036  brcoffn  40680  clsk3nimkb  40690  clsk1indlem1  40695  dvsconst  40982  dvsid  40983  dvsef  40984  islptre  42214  wallispilem1  42660  fourierdlem52  42753  ovnhoilem1  43193  gbowgt5  44233  gboge9  44235  nnsum3primesprm  44261  nnsum3primesgbe  44263  bgoldbnnsum3prm  44275  tgoldbachlt  44287  lincext1  44816  linds0  44827  lindsrng01  44830  lmod1lem3  44851  line2  45119  line2x  45121  inlinecirc02plem  45153  setrec1  45174
  Copyright terms: Public domain W3C validator