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

Theorem jctil 520
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 512 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 397
This theorem is referenced by:  jctl  524  nic-ax  1676  nic-axALT  1677  unidif  4876  iunxdif2  4984  exss  5379  xpiindi  5747  relssres  5935  frpoinsg  6250  nfunsn  6820  exfo  6990  fliftcnv  7191  oprres  7449  f1oweALT  7824  fo1stres  7866  fo2ndres  7867  dftpos3  8069  wfr3g  8147  tfrlem10  8227  odi  8419  omabs  8490  elixpsn  8734  sbthlem2  8880  sbthlem3  8881  fodomr  8924  mapxpen  8939  pssnn  8960  phplem2OLD  9010  pssnnOLD  9049  oieu  9307  inf3lem6  9400  frmin  9516  frr3g  9523  djuss  9687  acni3  9812  dfacacn  9906  kmlem1  9915  cflm  10015  cfsuc  10022  hsmexlem2  10192  hsmexlem4  10194  hsmexlem5  10195  axdc3lem4  10218  axcclem  10222  brdom5  10294  brdom4  10295  konigthlem  10333  alephval2  10337  alephmul  10343  wunex3  10506  reclem2pr  10813  suplem2pr  10818  lemulge11  11846  nn0ge2m1nn  12311  0mod  13631  1mod  13632  fzennn  13697  hashbclem  14173  hashge2el2dif  14203  wrdlenge2n0  14264  elovmptnn0wrd  14271  swrdnd  14376  s2f1o  14638  f1oun2prg  14639  cotrtrclfv  14732  resqrex  14971  modfsummods  15514  demoivreALT  15919  pcdiv  16562  prmodvdslcmf  16757  invsym2  17484  idghm  18858  gaid  18914  symgsubmefmndALT  19020  subrgid  20035  lbsextlem1  20429  mulgghm2  20707  smadiadet  21828  pmatcollpw3fi  21943  topcld  22195  ntrss  22215  restcld  22332  xkocnv  22974  fbssfi  22997  isfild  23018  alexsublem  23204  alexsubALTlem4  23210  metrest  23689  dscopn  23738  reconnlem1  23998  cphsubrglem  24350  cphipval  24416  itgcnlem  24963  vieta1  25481  jensen  26147  2lgs  26564  axlowdimlem6  27324  axlowdimlem7  27325  axlowdimlem16  27334  axlowdimlem17  27335  usgr2v1e2w  27628  0edg0rgr  27948  usgr2wlkspthlem2  28135  clwwlkf1  28422  0pthon  28500  ipval2  29078  sspg  29099  ssps  29101  sspmlem  29103  blocni  29176  ubthlem1  29241  bcsiALT  29550  ocsh  29654  chabs2  29888  pjoml6i  29960  osumcor2i  30015  nmopcoi  30466  opsqrlem6  30516  stlei  30611  mdslmd1lem1  30696  mdslmd2i  30701  atcvat3i  30767  atcvat4i  30768  sumdmdlem2  30790  dmdbr5ati  30793  xdivpnfrp  31216  oduprs  31251  tpr2rico  31871  ballotlemfp1  32467  ballotlemfc0  32468  ballotlemfcc  32469  ballotlemsup  32480  tgoldbachgt  32652  bnj545  32884  bnj548  32886  satfv1  33334  nosep1o  33893  nodense  33904  bdayimaon  33905  conway  34002  etasslt  34016  slerec  34022  cofcutr  34101  trer  34514  filnetlem3  34578  filnetlem4  34579  phpreu  35770  matunitlindflem1  35782  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem26  35812  mblfinlem1  35823  mblfinlem2  35824  mblfinlem3  35825  mblfinlem4  35826  ismblfin  35827  prter1  36900  pmapsub  37789  2xp3dxp2ge1d  40169  irrapx1  40657  dfacbasgrp  40940  dgraalem  40977  dgraaub  40980  brcoffn  41647  clsk3nimkb  41657  clsk1indlem1  41662  dvsconst  41955  dvsid  41956  dvsef  41957  islptre  43167  wallispilem1  43613  fourierdlem52  43706  ovnhoilem1  44146  gbowgt5  45225  gboge9  45227  nnsum3primesprm  45253  nnsum3primesgbe  45255  bgoldbnnsum3prm  45267  tgoldbachlt  45279  lincext1  45806  linds0  45817  lindsrng01  45820  lmod1lem3  45841  line2  46109  line2x  46111  inlinecirc02plem  46143  setrec1  46408
  Copyright terms: Public domain W3C validator