Theorem jctil 519

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 511	1 ⊢ (𝜑 → (𝜒 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  jctl  523  nic-ax  1674  nic-axALT  1675  unidif  4893  iunxdif2  5002  exss  5403  xpiindi  5775  relssres  5971  frpoinsg  6290  nfunsn  6861  exfo  7038  fliftcnv  7245  oprres  7514  f1oweALT  7904  fo1stres  7947  fo2ndres  7948  dftpos3  8174  wfr3g  8249  tfrlem10  8306  odi  8494  omabs  8566  elixpsn  8861  sbthlem2  9001  sbthlem3  9002  fodomr  9041  mapxpen  9056  pssnn  9078  oieu  9425  inf3lem6  9523  frmin  9642  frr3g  9649  djuss  9813  acni3  9938  dfacacn  10033  kmlem1  10042  cflm  10141  cfsuc  10148  hsmexlem2  10318  hsmexlem4  10320  hsmexlem5  10321  axdc3lem4  10344  axcclem  10348  brdom5  10420  brdom4  10421  konigthlem  10459  alephval2  10463  alephmul  10469  wunex3  10632  reclem2pr  10939  suplem2pr  10944  lemulge11  11984  nn0ge2m1nn  12451  0mod  13806  1mod  13807  fzennn  13875  hashbclem  14359  hashge2el2dif  14387  wrdlenge2n0  14459  elovmptnn0wrd  14466  swrdnd  14562  s2f1o  14823  f1oun2prg  14824  cotrtrclfv  14919  resqrex  15157  modfsummods  15700  demoivreALT  16110  pcdiv  16764  prmodvdslcmf  16959  invsym2  17670  oduprs  18206  chnexg  18524  idghm  19144  gaid  19212  symgsubmefmndALT  19316  subrgid  20489  lbsextlem1  21096  mulgghm2  21414  smadiadet  22586  pmatcollpw3fi  22701  topcld  22951  ntrss  22971  restcld  23088  xkocnv  23730  fbssfi  23753  isfild  23774  alexsublem  23960  alexsubALTlem4  23966  metrest  24440  dscopn  24489  reconnlem1  24743  cphsubrglem  25105  cphipval  25171  itgcnlem  25719  vieta1  26248  jensen  26927  2lgs  27346  nosep1o  27621  nodense  27632  bdayimaon  27633  conway  27741  etasslt  27755  slerec  27761  cofcutr  27869  om2noseqoi  28234  axlowdimlem6  28926  axlowdimlem7  28927  axlowdimlem16  28936  axlowdimlem17  28937  usgr2v1e2w  29231  0edg0rgr  29552  usgr2wlkspthlem2  29737  clwwlkf1  30027  0pthon  30105  ipval2  30685  sspg  30706  ssps  30708  sspmlem  30710  blocni  30783  ubthlem1  30848  bcsiALT  31157  ocsh  31261  chabs2  31495  pjoml6i  31567  osumcor2i  31622  nmopcoi  32073  opsqrlem6  32123  stlei  32218  mdslmd1lem1  32303  mdslmd2i  32308  atcvat3i  32374  atcvat4i  32375  sumdmdlem2  32397  dmdbr5ati  32400  xdivpnfrp  32911  fzo0pmtrlast  33059  tpr2rico  33923  ballotlemfp1  34503  ballotlemfc0  34504  ballotlemfcc  34505  ballotlemsup  34516  tgoldbachgt  34674  bnj545  34905  bnj548  34907  fineqvnttrclse  35142  wevgblacfn  35151  satfv1  35405  trer  36356  filnetlem3  36420  filnetlem4  36421  phpreu  37650  matunitlindflem1  37662  poimirlem16  37682  poimirlem17  37683  poimirlem19  37685  poimirlem20  37686  poimirlem26  37692  mblfinlem1  37703  mblfinlem2  37704  mblfinlem3  37705  mblfinlem4  37706  ismblfin  37707  prter1  38924  pmapsub  39813  irrapx1  42867  dfacbasgrp  43147  dgraalem  43184  dgraaub  43187  onexlimgt  43282  cantnftermord  43359  oacl2g  43369  onmcl  43370  omabs2  43371  omcl2  43372  ofoaf  43394  naddwordnexlem3  43438  naddwordnexlem4  43440  brcoffn  44069  clsk3nimkb  44079  clsk1indlem1  44084  dvsconst  44369  dvsid  44370  dvsef  44371  islptre  45665  wallispilem1  46109  fourierdlem52  46202  ovnhoilem1  46645  gbowgt5  47799  gboge9  47801  nnsum3primesprm  47827  nnsum3primesgbe  47829  bgoldbnnsum3prm  47841  tgoldbachlt  47853  stgrnbgr0  48001  grlicref  48049  gpgedg2ov  48103  pgnbgreunbgr  48162  lincext1  48492  linds0  48503  lindsrng01  48506  lmod1lem3  48527  line2  48790  line2x  48792  inlinecirc02plem  48824  2oppf  49170  setrec1  49729