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

Theorem jctil 557
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 552 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  jctl  561  nic-ax  1588  nic-axALT  1589  unidif  4401  iunxdif2  4498  exss  4852  xpiindi  5167  relssres  5344  nfunsn  6120  exfo  6270  fliftcnv  6439  oprres  6678  f1oweALT  7021  fo1stres  7061  fo2ndres  7062  dftpos3  7235  wfr3g  7278  tfrlem10  7348  odi  7524  omabs  7592  elixpsn  7811  sbthlem2  7934  sbthlem3  7935  fodomr  7974  mapxpen  7989  phplem2  8003  pssnn  8041  oieu  8305  inf3lem6  8391  acni3  8731  dfacacn  8824  kmlem1  8833  cflm  8933  cfsuc  8940  hsmexlem2  9110  hsmexlem4  9112  hsmexlem5  9113  axdc3lem4  9136  axcclem  9140  brdom5  9210  brdom4  9211  konigthlem  9247  alephval2  9251  alephmul  9257  wunex3  9420  reclem2pr  9727  suplem2pr  9732  lemulge11  10737  nn0ge2m1nn  11210  0mod  12521  1mod  12522  fzennn  12587  hashbclem  13048  hashge2el2dif  13070  wrdlenge2n0  13145  elovmptnn0wrd  13152  swrdnd  13233  2swrdeqwrdeq  13254  repswcshw  13358  s2f1o  13460  f1oun2prg  13461  cotrtrclfv  13550  resqrex  13788  demoivreALT  14719  pcdiv  15344  prmodvdslcmf  15538  invsym2  16195  idghm  17447  gaid  17504  subrgid  18554  lbsextlem1  18928  mulgghm2  19612  smadiadet  20243  pmatcollpw3fi  20357  topcld  20597  ntrss  20617  restcld  20734  xkocnv  21375  fbssfi  21399  isfild  21420  alexsublem  21606  alexsubALTlem4  21612  metrest  22087  dscopn  22136  reconnlem1  22385  cphsubrglem  22730  cphipval  22795  itgcnlem  23307  vieta1  23816  jensen  24460  2lgs  24877  axlowdimlem6  25573  axlowdimlem7  25574  axlowdimlem16  25583  axlowdimlem17  25584  cusgrafilem1  25801  0trlon  25872  2trllemE  25877  1pthon2v  25917  3v3e3cycl1  25966  4cycl4v4e  25988  4cycl4dv  25989  1conngra  25997  clwwlkf1  26118  usg2cwwkdifex  26143  numclwwlkovf2ex  26407  nvge0  26735  ipval2  26775  sspg  26799  ssps  26801  sspmlem  26803  blocni  26878  ubthlem1  26944  bcsiALT  27254  ocsh  27360  chabs2  27594  pjoml6i  27666  osumcor2i  27721  nmopcoi  28172  opsqrlem6  28222  stlei  28317  mdslmd1lem1  28402  mdslmd2i  28407  atcvat3i  28473  atcvat4i  28474  sumdmdlem2  28496  dmdbr5ati  28499  xdivpnfrp  28806  oduprs  28821  tpr2rico  29120  ballotlemfp1  29714  ballotlemfc0  29715  ballotlemfcc  29716  ballotlemsup  29727  bnj545  30053  bnj548  30055  fv1stcnv  30759  fv2ndcnv  30760  frr3g  30857  nodense  30922  nobndlem1  30925  nobnddown  30934  nofulllem3  30937  trer  31314  filnetlem3  31379  filnetlem4  31380  phpreu  32387  matunitlindflem1  32399  poimirlem16  32419  poimirlem17  32420  poimirlem19  32422  poimirlem20  32423  poimirlem26  32429  mblfinlem1  32440  mblfinlem2  32441  mblfinlem3  32442  mblfinlem4  32443  ismblfin  32444  prter1  33006  pmapsub  33896  irrapx1  36234  dfacbasgrp  36521  dgraalem  36558  dgraaub  36561  brcoffn  37172  clsk3nimkb  37182  clsk1indlem1  37187  dvsconst  37375  dvsid  37376  dvsef  37377  islptre  38510  wallispilem1  38782  fourierdlem52  38875  ovnhoilem1  39315  gbogt5  40009  gboage9  40011  nnsum3primesprm  40031  nnsum3primesgbe  40033  bgoldbnnsum3prm  40045  tgoldbachlt  40055  tgoldbachltOLD  40062  usgr2v1e2w  40500  0edg0rgr  40794  usgr2wlkspthlem2  40986  clwwlksf1  41246  0pthon-av  41317  av-numclwwlkovf2ex  41539  lincext1  42059  linds0  42070  lindsrng01  42073  lmod1lem3  42094
  Copyright terms: Public domain W3C validator