Theorem jctil 558

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

Step	Hyp	Ref	Expression
1		jctil.2	. . 3 ⊢ 𝜒
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝜒)
3		jctil.1	. 2 ⊢ (𝜑 → 𝜓)
4	2, 3	jca 553	1 ⊢ (𝜑 → (𝜒 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  jctl  562  nic-ax  1589  nic-axALT  1590  unidif  4407  iunxdif2  4504  exss  4858  xpiindi  5179  relssres  5357  nfunsn  6135  exfo  6285  fliftcnv  6461  oprres  6700  f1oweALT  7043  fo1stres  7083  fo2ndres  7084  dftpos3  7257  wfr3g  7300  tfrlem10  7370  odi  7546  omabs  7614  elixpsn  7833  sbthlem2  7956  sbthlem3  7957  fodomr  7996  mapxpen  8011  phplem2  8025  pssnn  8063  oieu  8327  inf3lem6  8413  acni3  8753  dfacacn  8846  kmlem1  8855  cflm  8955  cfsuc  8962  hsmexlem2  9132  hsmexlem4  9134  hsmexlem5  9135  axdc3lem4  9158  axcclem  9162  brdom5  9232  brdom4  9233  konigthlem  9269  alephval2  9273  alephmul  9279  wunex3  9442  reclem2pr  9749  suplem2pr  9754  lemulge11  10764  nn0ge2m1nn  11237  0mod  12563  1mod  12564  fzennn  12629  hashbclem  13093  hashge2el2dif  13117  wrdlenge2n0  13196  elovmptnn0wrd  13203  swrdnd  13284  2swrdeqwrdeq  13305  repswcshw  13409  s2f1o  13511  f1oun2prg  13512  cotrtrclfv  13601  resqrex  13839  demoivreALT  14770  pcdiv  15395  prmodvdslcmf  15589  invsym2  16246  idghm  17498  gaid  17555  subrgid  18605  lbsextlem1  18979  mulgghm2  19664  smadiadet  20295  pmatcollpw3fi  20409  topcld  20649  ntrss  20669  restcld  20786  xkocnv  21427  fbssfi  21451  isfild  21472  alexsublem  21658  alexsubALTlem4  21664  metrest  22139  dscopn  22188  reconnlem1  22437  cphsubrglem  22785  cphipval  22850  itgcnlem  23362  vieta1  23871  jensen  24515  2lgs  24932  axlowdimlem6  25627  axlowdimlem7  25628  axlowdimlem16  25637  axlowdimlem17  25638  cusgrafilem1  26007  0trlon  26078  2trllemE  26083  1pthon2v  26123  3v3e3cycl1  26172  4cycl4v4e  26194  4cycl4dv  26195  1conngra  26203  clwwlkf1  26324  usg2cwwkdifex  26349  numclwwlkovf2ex  26613  nvge0  26912  ipval2  26946  sspg  26967  ssps  26969  sspmlem  26971  blocni  27044  ubthlem1  27110  bcsiALT  27420  ocsh  27526  chabs2  27760  pjoml6i  27832  osumcor2i  27887  nmopcoi  28338  opsqrlem6  28388  stlei  28483  mdslmd1lem1  28568  mdslmd2i  28573  atcvat3i  28639  atcvat4i  28640  sumdmdlem2  28662  dmdbr5ati  28665  xdivpnfrp  28972  oduprs  28987  tpr2rico  29286  ballotlemfp1  29880  ballotlemfc0  29881  ballotlemfcc  29882  ballotlemsup  29893  bnj545  30219  bnj548  30221  fv1stcnv  30925  fv2ndcnv  30926  frr3g  31023  nodense  31088  nobndlem1  31091  nobnddown  31100  nofulllem3  31103  trer  31480  filnetlem3  31545  filnetlem4  31546  phpreu  32563  matunitlindflem1  32575  poimirlem16  32595  poimirlem17  32596  poimirlem19  32598  poimirlem20  32599  poimirlem26  32605  mblfinlem1  32616  mblfinlem2  32617  mblfinlem3  32618  mblfinlem4  32619  ismblfin  32620  prter1  33182  pmapsub  34072  irrapx1  36410  dfacbasgrp  36697  dgraalem  36734  dgraaub  36737  brcoffn  37348  clsk3nimkb  37358  clsk1indlem1  37363  dvsconst  37551  dvsid  37552  dvsef  37553  islptre  38686  wallispilem1  38958  fourierdlem52  39051  ovnhoilem1  39491  gbogt5  40184  gboage9  40186  nnsum3primesprm  40206  nnsum3primesgbe  40208  bgoldbnnsum3prm  40220  tgoldbachlt  40230  tgoldbachltOLD  40237  usgr2v1e2w  40478  0edg0rgr  40772  usgr2wlkspthlem2  40964  clwwlksf1  41224  0pthon-av  41295  av-numclwwlkovf2ex  41517  lincext1  42037  linds0  42048  lindsrng01  42051  lmod1lem3  42072  setrec1  42237