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 208  df-an 397
This theorem is referenced by:  jctl  524  nic-ax  1665  nic-axALT  1666  unidif  4865  iunxdif2  4969  exss  5347  xpiindi  5700  relssres  5887  nfunsn  6701  exfo  6864  fliftcnv  7053  oprres  7305  f1oweALT  7664  fo1stres  7706  fo2ndres  7707  dftpos3  7901  wfr3g  7944  tfrlem10  8014  odi  8195  omabs  8264  elixpsn  8490  sbthlem2  8617  sbthlem3  8618  fodomr  8657  mapxpen  8672  phplem2  8686  pssnn  8725  oieu  8992  inf3lem6  9085  djuss  9338  acni3  9462  dfacacn  9556  kmlem1  9565  cflm  9661  cfsuc  9668  hsmexlem2  9838  hsmexlem4  9840  hsmexlem5  9841  axdc3lem4  9864  axcclem  9868  brdom5  9940  brdom4  9941  konigthlem  9979  alephval2  9983  alephmul  9989  wunex3  10152  reclem2pr  10459  suplem2pr  10464  lemulge11  11491  nn0ge2m1nn  11953  0mod  13260  1mod  13261  fzennn  13326  hashbclem  13800  hashge2el2dif  13828  wrdlenge2n0  13894  elovmptnn0wrd  13901  swrdnd  14006  s2f1o  14268  f1oun2prg  14269  cotrtrclfv  14362  resqrex  14600  modfsummods  15138  demoivreALT  15544  pcdiv  16179  prmodvdslcmf  16373  invsym2  17023  idghm  18313  gaid  18369  subrgid  19468  lbsextlem1  19861  mulgghm2  20574  smadiadet  21209  pmatcollpw3fi  21323  topcld  21573  ntrss  21593  restcld  21710  xkocnv  22352  fbssfi  22375  isfild  22396  alexsublem  22582  alexsubALTlem4  22588  metrest  23063  dscopn  23112  reconnlem1  23363  cphsubrglem  23710  cphipval  23775  itgcnlem  24319  vieta1  24830  jensen  25494  2lgs  25911  axlowdimlem6  26661  axlowdimlem7  26662  axlowdimlem16  26671  axlowdimlem17  26672  usgr2v1e2w  26962  0edg0rgr  27282  usgr2wlkspthlem2  27467  clwwlkf1  27756  0pthon  27834  ipval2  28412  sspg  28433  ssps  28435  sspmlem  28437  blocni  28510  ubthlem1  28575  bcsiALT  28884  ocsh  28988  chabs2  29222  pjoml6i  29294  osumcor2i  29349  nmopcoi  29800  opsqrlem6  29850  stlei  29945  mdslmd1lem1  30030  mdslmd2i  30035  atcvat3i  30101  atcvat4i  30102  sumdmdlem2  30124  dmdbr5ati  30127  xdivpnfrp  30537  oduprs  30571  tpr2rico  31055  ballotlemfp1  31649  ballotlemfc0  31650  ballotlemfcc  31651  ballotlemsup  31662  tgoldbachgt  31834  bnj545  32067  bnj548  32069  satfv1  32508  frpoinsg  32979  frr3g  33019  nosep1o  33084  nodense  33094  bdayimaon  33095  nulsslt  33160  conway  33162  etasslt  33172  slerec  33175  trer  33562  filnetlem3  33626  filnetlem4  33627  phpreu  34758  matunitlindflem1  34770  poimirlem16  34790  poimirlem17  34791  poimirlem19  34793  poimirlem20  34794  poimirlem26  34800  mblfinlem1  34811  mblfinlem2  34812  mblfinlem3  34813  mblfinlem4  34814  ismblfin  34815  prter1  35897  pmapsub  36786  irrapx1  39305  dfacbasgrp  39588  dgraalem  39625  dgraaub  39628  brcoffn  40260  clsk3nimkb  40270  clsk1indlem1  40275  dvsconst  40542  dvsid  40543  dvsef  40544  islptre  41780  wallispilem1  42231  fourierdlem52  42324  ovnhoilem1  42764  gbowgt5  43774  gboge9  43776  nnsum3primesprm  43802  nnsum3primesgbe  43804  bgoldbnnsum3prm  43816  tgoldbachlt  43828  lincext1  44407  linds0  44418  lindsrng01  44421  lmod1lem3  44442  line2  44637  line2x  44639  inlinecirc02plem  44671  setrec1  44692
  Copyright terms: Public domain W3C validator