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

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

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 206  df-an 397

This theorem is referenced by:  jctl  524  nic-ax  1680  nic-axALT  1681  unidif  4881  iunxdif2  4988  exss  5382  xpiindi  5743  relssres  5931  frpoinsg  6245  nfunsn  6808  exfo  6978  fliftcnv  7179  oprres  7435  f1oweALT  7809  fo1stres  7851  fo2ndres  7852  dftpos3  8052  wfr3g  8130  tfrlem10  8210  odi  8402  omabs  8473  elixpsn  8717  sbthlem2  8862  sbthlem3  8863  fodomr  8906  mapxpen  8921  pssnn  8942  phplem2OLD  8991  pssnnOLD  9028  oieu  9286  inf3lem6  9379  frmin  9517  frr3g  9525  djuss  9689  acni3  9814  dfacacn  9908  kmlem1  9917  cflm  10017  cfsuc  10024  hsmexlem2  10194  hsmexlem4  10196  hsmexlem5  10197  axdc3lem4  10220  axcclem  10224  brdom5  10296  brdom4  10297  konigthlem  10335  alephval2  10339  alephmul  10345  wunex3  10508  reclem2pr  10815  suplem2pr  10820  lemulge11  11848  nn0ge2m1nn  12313  0mod  13633  1mod  13634  fzennn  13699  hashbclem  14175  hashge2el2dif  14205  wrdlenge2n0  14266  elovmptnn0wrd  14273  swrdnd  14378  s2f1o  14640  f1oun2prg  14641  cotrtrclfv  14734  resqrex  14973  modfsummods  15516  demoivreALT  15921  pcdiv  16564  prmodvdslcmf  16759  invsym2  17486  idghm  18860  gaid  18916  symgsubmefmndALT  19022  subrgid  20037  lbsextlem1  20431  mulgghm2  20709  smadiadet  21830  pmatcollpw3fi  21945  topcld  22197  ntrss  22217  restcld  22334  xkocnv  22976  fbssfi  22999  isfild  23020  alexsublem  23206  alexsubALTlem4  23212  metrest  23691  dscopn  23740  reconnlem1  24000  cphsubrglem  24352  cphipval  24418  itgcnlem  24965  vieta1  25483  jensen  26149  2lgs  26566  axlowdimlem6  27326  axlowdimlem7  27327  axlowdimlem16  27336  axlowdimlem17  27337  usgr2v1e2w  27630  0edg0rgr  27950  usgr2wlkspthlem2  28135  clwwlkf1  28422  0pthon  28500  ipval2  29078  sspg  29099  ssps  29101  sspmlem  29103  blocni  29176  ubthlem1  29241  bcsiALT  29550  ocsh  29654  chabs2  29888  pjoml6i  29960  osumcor2i  30015  nmopcoi  30466  opsqrlem6  30516  stlei  30611  mdslmd1lem1  30696  mdslmd2i  30701  atcvat3i  30767  atcvat4i  30768  sumdmdlem2  30790  dmdbr5ati  30793  xdivpnfrp  31216  oduprs  31251  tpr2rico  31871  ballotlemfp1  32467  ballotlemfc0  32468  ballotlemfcc  32469  ballotlemsup  32480  tgoldbachgt  32652  bnj545  32884  bnj548  32886  satfv1  33334  nosep1o  33893  nodense  33904  bdayimaon  33905  conway  34002  etasslt  34016  slerec  34022  cofcutr  34101  trer  34514  filnetlem3  34578  filnetlem4  34579  phpreu  35770  matunitlindflem1  35782  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem26  35812  mblfinlem1  35823  mblfinlem2  35824  mblfinlem3  35825  mblfinlem4  35826  ismblfin  35827  prter1  36902  pmapsub  37791  2xp3dxp2ge1d  40171  irrapx1  40659  dfacbasgrp  40942  dgraalem  40979  dgraaub  40982  brcoffn  41622  clsk3nimkb  41632  clsk1indlem1  41637  dvsconst  41930  dvsid  41931  dvsef  41932  islptre  43142  wallispilem1  43588  fourierdlem52  43681  ovnhoilem1  44121  gbowgt5  45193  gboge9  45195  nnsum3primesprm  45221  nnsum3primesgbe  45223  bgoldbnnsum3prm  45235  tgoldbachlt  45247  lincext1  45774  linds0  45785  lindsrng01  45788  lmod1lem3  45809  line2  46077  line2x  46079  inlinecirc02plem  46111  setrec1  46376