Theorem jctil 524

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 516	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 208  df-an 397

This theorem is referenced by:  jctl  528  nic-ax  1680  nic-axALT  1681  unidif  4880  iunxdif2  4990  exss  5409  xpiindi  5784  relssres  5981  frpoinsg  6301  nfunsn  6873  exfo  7053  fliftcnv  7262  oprres  7531  f1oweALT  7921  fo1stres  7964  fo2ndres  7965  dftpos3  8191  wfr3g  8266  tfrlem10  8323  odi  8511  omabs  8584  elixpsn  8882  sbthlem2  9023  sbthlem3  9024  fodomr  9063  mapxpen  9078  pssnn  9100  oieu  9451  inf3lem6  9552  frmin  9671  frr3g  9678  djuss  9842  acni3  9967  dfacacn  10062  kmlem1  10071  cflm  10170  cfsuc  10177  hsmexlem2  10347  hsmexlem4  10349  hsmexlem5  10350  axdc3lem4  10373  axcclem  10377  brdom5  10449  brdom4  10450  konigthlem  10489  alephval2  10493  alephmul  10499  wunex3  10662  reclem2pr  10969  suplem2pr  10974  lemulge11  12016  nn0ge2m1nn  12505  0mod  13859  1mod  13860  fzennn  13928  hashbclem  14412  hashge2el2dif  14440  wrdlenge2n0  14512  elovmptnn0wrd  14519  swrdnd  14615  s2f1o  14876  f1oun2prg  14877  cotrtrclfv  14972  resqrex  15210  modfsummods  15754  demoivreALT  16166  pcdiv  16821  prmodvdslcmf  17016  invsym2  17728  oduprs  18264  chnexg  18582  idghm  19204  gaid  19272  symgsubmefmndALT  19376  subrgid  20552  lbsextlem1  21158  mulgghm2  21458  smadiadet  22660  pmatcollpw3fi  22775  topcld  23025  ntrss  23045  restcld  23162  xkocnv  23804  fbssfi  23827  isfild  23848  alexsublem  24034  alexsubALTlem4  24040  metrest  24514  dscopn  24563  reconnlem1  24817  cphsubrglem  25169  cphipval  25235  itgcnlem  25782  vieta1  26303  jensen  26977  2lgs  27395  nosep1o  27670  nodense  27681  bdayimaon  27682  conway  27796  etaslts  27810  lesrec  27816  cofcutr  27941  om2noseqoi  28320  axlowdimlem6  29041  axlowdimlem7  29042  axlowdimlem16  29051  axlowdimlem17  29052  usgr2v1e2w  29346  0edg0rgr  29666  usgr2wlkspthlem2  29851  clwwlkf1  30144  0pthon  30222  ipval2  30803  sspg  30824  ssps  30826  sspmlem  30828  blocni  30901  ubthlem1  30966  bcsiALT  31275  ocsh  31379  chabs2  31613  pjoml6i  31685  osumcor2i  31740  nmopcoi  32191  opsqrlem6  32241  stlei  32336  mdslmd1lem1  32421  mdslmd2i  32426  atcvat3i  32492  atcvat4i  32493  sumdmdlem2  32515  dmdbr5ati  32518  xdivpnfrp  33018  fzo0pmtrlast  33180  tpr2rico  34103  ballotlemfp1  34683  ballotlemfc0  34684  ballotlemfcc  34685  ballotlemsup  34696  tgoldbachgt  34854  bnj545  35084  bnj548  35086  fineqvnttrclse  35312  wevgblacfn  35344  satfv1  35598  trer  36551  filnetlem3  36615  filnetlem4  36616  phpreu  37978  matunitlindflem1  37990  poimirlem16  38010  poimirlem17  38011  poimirlem19  38013  poimirlem20  38014  poimirlem26  38020  mblfinlem1  38031  mblfinlem2  38032  mblfinlem3  38033  mblfinlem4  38034  ismblfin  38035  prter1  39378  pmapsub  40267  irrapx1  43280  dfacbasgrp  43560  dgraalem  43597  dgraaub  43600  onexlimgt  43695  cantnftermord  43772  oacl2g  43782  onmcl  43783  omabs2  43784  omcl2  43785  ofoaf  43807  naddwordnexlem3  43851  naddwordnexlem4  43853  brcoffn  44481  clsk3nimkb  44491  clsk1indlem1  44496  dvsconst  44781  dvsid  44782  dvsef  44783  islptre  46071  wallispilem1  46515  fourierdlem52  46608  ovnhoilem1  47051  nprmmul3  48011  gbowgt5  48260  gboge9  48262  nnsum3primesprm  48288  nnsum3primesgbe  48290  bgoldbnnsum3prm  48302  tgoldbachlt  48314  stgrnbgr0  48462  grlicref  48510  gpgedg2ov  48564  pgnbgreunbgr  48623  lincext1  48952  linds0  48963  lindsrng01  48966  lmod1lem3  48987  line2  49250  line2x  49252  inlinecirc02plem  49284  2oppf  49629  setrec1  50188