Theorem jctil 511

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

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

This theorem is referenced by:  jctl  515  nic-ax  1753  nic-axALT  1754  unidif  4665  iunxdif2  4760  exss  5121  xpiindi  5459  relssres  5641  nfunsn  6441  exfo  6595  fliftcnv  6781  oprres  7028  f1oweALT  7378  fo1stres  7420  fo2ndres  7421  dftpos3  7601  wfr3g  7644  tfrlem10  7715  odi  7892  omabs  7960  elixpsn  8180  sbthlem2  8306  sbthlem3  8307  fodomr  8346  mapxpen  8361  phplem2  8375  pssnn  8413  oieu  8679  inf3lem6  8773  djuss  9025  acni3  9149  dfacacn  9244  kmlem1  9253  cflm  9353  cfsuc  9360  hsmexlem2  9530  hsmexlem4  9532  hsmexlem5  9533  axdc3lem4  9556  axcclem  9560  brdom5  9632  brdom4  9633  konigthlem  9671  alephval2  9675  alephmul  9681  wunex3  9844  reclem2pr  10151  suplem2pr  10156  lemulge11  11166  nn0ge2m1nn  11622  0mod  12921  1mod  12922  fzennn  12987  hashbclem  13449  hashge2el2dif  13475  wrdlenge2n0  13549  elovmptnn0wrd  13556  swrdnd  13652  2swrdeqwrdeq  13673  repswcshw  13778  s2f1o  13881  f1oun2prg  13882  cotrtrclfv  13972  resqrex  14210  modfsummods  14743  demoivreALT  15147  pcdiv  15770  prmodvdslcmf  15964  invsym2  16623  idghm  17873  gaid  17929  subrgid  18982  lbsextlem1  19363  mulgghm2  20049  smadiadet  20685  pmatcollpw3fi  20800  topcld  21050  ntrss  21070  restcld  21187  xkocnv  21828  fbssfi  21851  isfild  21872  alexsublem  22058  alexsubALTlem4  22064  metrest  22539  dscopn  22588  reconnlem1  22839  cphsubrglem  23186  cphipval  23251  itgcnlem  23769  vieta1  24280  jensen  24928  2lgs  25345  axlowdimlem6  26040  axlowdimlem7  26041  axlowdimlem16  26050  axlowdimlem17  26051  usgr2v1e2w  26359  0edg0rgr  26695  usgr2wlkspthlem2  26881  clwwlkf1  27197  0pthon  27299  ipval2  27889  sspg  27910  ssps  27912  sspmlem  27914  blocni  27987  ubthlem1  28053  bcsiALT  28363  ocsh  28469  chabs2  28703  pjoml6i  28775  osumcor2i  28830  nmopcoi  29281  opsqrlem6  29331  stlei  29426  mdslmd1lem1  29511  mdslmd2i  29516  atcvat3i  29582  atcvat4i  29583  sumdmdlem2  29605  dmdbr5ati  29608  xdivpnfrp  29965  oduprs  29980  tpr2rico  30282  ballotlemfp1  30877  ballotlemfc0  30878  ballotlemfcc  30879  ballotlemsup  30890  tgoldbachgt  31065  bnj545  31286  bnj548  31288  fv1stcnv  31998  fv2ndcnv  31999  frpoinsg  32060  frr3g  32098  nosep1o  32151  nodense  32161  bdayimaon  32162  nulsslt  32227  conway  32229  etasslt  32239  slerec  32242  trer  32629  filnetlem3  32694  filnetlem4  32695  phpreu  33704  matunitlindflem1  33716  poimirlem16  33736  poimirlem17  33737  poimirlem19  33739  poimirlem20  33740  poimirlem26  33746  mblfinlem1  33757  mblfinlem2  33758  mblfinlem3  33759  mblfinlem4  33760  ismblfin  33761  prter1  34656  pmapsub  35546  irrapx1  37891  dfacbasgrp  38176  dgraalem  38213  dgraaub  38216  brcoffn  38825  clsk3nimkb  38835  clsk1indlem1  38840  dvsconst  39026  dvsid  39027  dvsef  39028  islptre  40328  wallispilem1  40758  fourierdlem52  40851  ovnhoilem1  41294  gbowgt5  42222  gboge9  42224  nnsum3primesprm  42250  nnsum3primesgbe  42252  bgoldbnnsum3prm  42264  tgoldbachlt  42276  lincext1  42808  linds0  42819  lindsrng01  42822  lmod1lem3  42843  setrec1  43003