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  4898  iunxdif2  5009  exss  5411  xpiindi  5784  relssres  5981  frpoinsg  6301  nfunsn  6873  exfo  7050  fliftcnv  7257  oprres  7526  f1oweALT  7916  fo1stres  7959  fo2ndres  7960  dftpos3  8186  wfr3g  8261  tfrlem10  8318  odi  8506  omabs  8579  elixpsn  8875  sbthlem2  9016  sbthlem3  9017  fodomr  9056  mapxpen  9071  pssnn  9093  oieu  9444  inf3lem6  9542  frmin  9661  frr3g  9668  djuss  9832  acni3  9957  dfacacn  10052  kmlem1  10061  cflm  10160  cfsuc  10167  hsmexlem2  10337  hsmexlem4  10339  hsmexlem5  10340  axdc3lem4  10363  axcclem  10367  brdom5  10439  brdom4  10440  konigthlem  10479  alephval2  10483  alephmul  10489  wunex3  10652  reclem2pr  10959  suplem2pr  10964  lemulge11  12004  nn0ge2m1nn  12471  0mod  13822  1mod  13823  fzennn  13891  hashbclem  14375  hashge2el2dif  14403  wrdlenge2n0  14475  elovmptnn0wrd  14482  swrdnd  14578  s2f1o  14839  f1oun2prg  14840  cotrtrclfv  14935  resqrex  15173  modfsummods  15716  demoivreALT  16126  pcdiv  16780  prmodvdslcmf  16975  invsym2  17687  oduprs  18223  chnexg  18541  idghm  19160  gaid  19228  symgsubmefmndALT  19332  subrgid  20506  lbsextlem1  21113  mulgghm2  21431  smadiadet  22614  pmatcollpw3fi  22729  topcld  22979  ntrss  22999  restcld  23116  xkocnv  23758  fbssfi  23781  isfild  23802  alexsublem  23988  alexsubALTlem4  23994  metrest  24468  dscopn  24517  reconnlem1  24771  cphsubrglem  25133  cphipval  25199  itgcnlem  25747  vieta1  26276  jensen  26955  2lgs  27374  nosep1o  27649  nodense  27660  bdayimaon  27661  conway  27775  etaslts  27789  lesrec  27795  cofcutr  27920  om2noseqoi  28299  axlowdimlem6  29020  axlowdimlem7  29021  axlowdimlem16  29030  axlowdimlem17  29031  usgr2v1e2w  29325  0edg0rgr  29646  usgr2wlkspthlem2  29831  clwwlkf1  30124  0pthon  30202  ipval2  30782  sspg  30803  ssps  30805  sspmlem  30807  blocni  30880  ubthlem1  30945  bcsiALT  31254  ocsh  31358  chabs2  31592  pjoml6i  31664  osumcor2i  31719  nmopcoi  32170  opsqrlem6  32220  stlei  32315  mdslmd1lem1  32400  mdslmd2i  32405  atcvat3i  32471  atcvat4i  32472  sumdmdlem2  32494  dmdbr5ati  32497  xdivpnfrp  33014  fzo0pmtrlast  33174  tpr2rico  34069  ballotlemfp1  34649  ballotlemfc0  34650  ballotlemfcc  34651  ballotlemsup  34662  tgoldbachgt  34820  bnj545  35051  bnj548  35053  fineqvnttrclse  35280  wevgblacfn  35303  satfv1  35557  trer  36510  filnetlem3  36574  filnetlem4  36575  phpreu  37805  matunitlindflem1  37817  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem26  37847  mblfinlem1  37858  mblfinlem2  37859  mblfinlem3  37860  mblfinlem4  37861  ismblfin  37862  prter1  39139  pmapsub  40028  irrapx1  43070  dfacbasgrp  43350  dgraalem  43387  dgraaub  43390  onexlimgt  43485  cantnftermord  43562  oacl2g  43572  onmcl  43573  omabs2  43574  omcl2  43575  ofoaf  43597  naddwordnexlem3  43641  naddwordnexlem4  43643  brcoffn  44271  clsk3nimkb  44281  clsk1indlem1  44286  dvsconst  44571  dvsid  44572  dvsef  44573  islptre  45865  wallispilem1  46309  fourierdlem52  46402  ovnhoilem1  46845  gbowgt5  48008  gboge9  48010  nnsum3primesprm  48036  nnsum3primesgbe  48038  bgoldbnnsum3prm  48050  tgoldbachlt  48062  stgrnbgr0  48210  grlicref  48258  gpgedg2ov  48312  pgnbgreunbgr  48371  lincext1  48700  linds0  48711  lindsrng01  48714  lmod1lem3  48735  line2  48998  line2x  49000  inlinecirc02plem  49032  2oppf  49377  setrec1  49936