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

Theorem jctil 559
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 554 1 (𝜑 → (𝜒𝜓))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 197  df-an 386
This theorem is referenced by:  jctl  563  nic-ax  1596  nic-axALT  1597  unidif  4462  iunxdif2  4559  exss  4922  xpiindi  5246  relssres  5425  nfunsn  6212  exfo  6363  fliftcnv  6546  oprres  6787  f1oweALT  7137  fo1stres  7177  fo2ndres  7178  dftpos3  7355  wfr3g  7398  tfrlem10  7468  odi  7644  omabs  7712  elixpsn  7932  sbthlem2  8056  sbthlem3  8057  fodomr  8096  mapxpen  8111  phplem2  8125  pssnn  8163  oieu  8429  inf3lem6  8515  acni3  8855  dfacacn  8948  kmlem1  8957  cflm  9057  cfsuc  9064  hsmexlem2  9234  hsmexlem4  9236  hsmexlem5  9237  axdc3lem4  9260  axcclem  9264  brdom5  9336  brdom4  9337  konigthlem  9375  alephval2  9379  alephmul  9385  wunex3  9548  reclem2pr  9855  suplem2pr  9860  lemulge11  10870  nn0ge2m1nn  11345  0mod  12684  1mod  12685  fzennn  12750  hashbclem  13219  hashge2el2dif  13245  wrdlenge2n0  13324  elovmptnn0wrd  13331  swrdnd  13414  2swrdeqwrdeq  13435  repswcshw  13539  s2f1o  13642  f1oun2prg  13643  cotrtrclfv  13734  resqrex  13972  modfsummods  14506  demoivreALT  14912  pcdiv  15538  prmodvdslcmf  15732  invsym2  16404  idghm  17656  gaid  17713  subrgid  18763  lbsextlem1  19139  mulgghm2  19826  smadiadet  20457  pmatcollpw3fi  20571  topcld  20820  ntrss  20840  restcld  20957  xkocnv  21598  fbssfi  21622  isfild  21643  alexsublem  21829  alexsubALTlem4  21835  metrest  22310  dscopn  22359  reconnlem1  22610  cphsubrglem  22958  cphipval  23023  itgcnlem  23537  vieta1  24048  jensen  24696  2lgs  25113  axlowdimlem6  25808  axlowdimlem7  25809  axlowdimlem16  25818  axlowdimlem17  25819  usgr2v1e2w  26125  0edg0rgr  26449  usgr2wlkspthlem2  26635  clwwlksf1  26897  0pthon  26968  numclwwlkovf2ex  27191  nvge0  27498  ipval2  27532  sspg  27553  ssps  27555  sspmlem  27557  blocni  27630  ubthlem1  27696  bcsiALT  28006  ocsh  28112  chabs2  28346  pjoml6i  28418  osumcor2i  28473  nmopcoi  28924  opsqrlem6  28974  stlei  29069  mdslmd1lem1  29154  mdslmd2i  29159  atcvat3i  29225  atcvat4i  29226  sumdmdlem2  29248  dmdbr5ati  29251  xdivpnfrp  29615  oduprs  29630  tpr2rico  29932  ballotlemfp1  30527  ballotlemfc0  30528  ballotlemfcc  30529  ballotlemsup  30540  tgoldbachgt  30715  bnj545  30939  bnj548  30941  fv1stcnv  31654  fv2ndcnv  31655  frr3g  31753  nosep1o  31806  nodense  31816  bdayimaon  31817  nulsslt  31882  conway  31884  etasslt  31894  slerec  31897  trer  32285  filnetlem3  32350  filnetlem4  32351  phpreu  33364  matunitlindflem1  33376  poimirlem16  33396  poimirlem17  33397  poimirlem19  33399  poimirlem20  33400  poimirlem26  33406  mblfinlem1  33417  mblfinlem2  33418  mblfinlem3  33419  mblfinlem4  33420  ismblfin  33421  prter1  33983  pmapsub  34873  irrapx1  37211  dfacbasgrp  37497  dgraalem  37534  dgraaub  37537  brcoffn  38148  clsk3nimkb  38158  clsk1indlem1  38163  dvsconst  38349  dvsid  38350  dvsef  38351  islptre  39651  wallispilem1  40045  fourierdlem52  40138  ovnhoilem1  40578  gbowgt5  41415  gboge9  41417  nnsum3primesprm  41443  nnsum3primesgbe  41445  bgoldbnnsum3prm  41457  tgoldbachlt  41469  tgoldbachltOLD  41475  lincext1  42008  linds0  42019  lindsrng01  42022  lmod1lem3  42043  setrec1  42203
  Copyright terms: Public domain W3C validator