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  1675  nic-axALT  1676  unidif  4885  iunxdif2  4996  exss  5415  xpiindi  5790  relssres  5987  frpoinsg  6307  nfunsn  6879  exfo  7057  fliftcnv  7266  oprres  7535  f1oweALT  7925  fo1stres  7968  fo2ndres  7969  dftpos3  8194  wfr3g  8269  tfrlem10  8326  odi  8514  omabs  8587  elixpsn  8885  sbthlem2  9026  sbthlem3  9027  fodomr  9066  mapxpen  9081  pssnn  9103  oieu  9454  inf3lem6  9554  frmin  9673  frr3g  9680  djuss  9844  acni3  9969  dfacacn  10064  kmlem1  10073  cflm  10172  cfsuc  10179  hsmexlem2  10349  hsmexlem4  10351  hsmexlem5  10352  axdc3lem4  10375  axcclem  10379  brdom5  10451  brdom4  10452  konigthlem  10491  alephval2  10495  alephmul  10501  wunex3  10664  reclem2pr  10971  suplem2pr  10976  lemulge11  12018  nn0ge2m1nn  12507  0mod  13861  1mod  13862  fzennn  13930  hashbclem  14414  hashge2el2dif  14442  wrdlenge2n0  14514  elovmptnn0wrd  14521  swrdnd  14617  s2f1o  14878  f1oun2prg  14879  cotrtrclfv  14974  resqrex  15212  modfsummods  15756  demoivreALT  16168  pcdiv  16823  prmodvdslcmf  17018  invsym2  17730  oduprs  18266  chnexg  18584  idghm  19206  gaid  19274  symgsubmefmndALT  19378  subrgid  20550  lbsextlem1  21156  mulgghm2  21456  smadiadet  22635  pmatcollpw3fi  22750  topcld  23000  ntrss  23020  restcld  23137  xkocnv  23779  fbssfi  23802  isfild  23823  alexsublem  24009  alexsubALTlem4  24015  metrest  24489  dscopn  24538  reconnlem1  24792  cphsubrglem  25144  cphipval  25210  itgcnlem  25757  vieta1  26278  jensen  26952  2lgs  27370  nosep1o  27645  nodense  27656  bdayimaon  27657  conway  27771  etaslts  27785  lesrec  27791  cofcutr  27916  om2noseqoi  28295  axlowdimlem6  29016  axlowdimlem7  29017  axlowdimlem16  29026  axlowdimlem17  29027  usgr2v1e2w  29321  0edg0rgr  29641  usgr2wlkspthlem2  29826  clwwlkf1  30119  0pthon  30197  ipval2  30778  sspg  30799  ssps  30801  sspmlem  30803  blocni  30876  ubthlem1  30941  bcsiALT  31250  ocsh  31354  chabs2  31588  pjoml6i  31660  osumcor2i  31715  nmopcoi  32166  opsqrlem6  32216  stlei  32311  mdslmd1lem1  32396  mdslmd2i  32401  atcvat3i  32467  atcvat4i  32468  sumdmdlem2  32490  dmdbr5ati  32493  xdivpnfrp  32992  fzo0pmtrlast  33153  tpr2rico  34056  ballotlemfp1  34636  ballotlemfc0  34637  ballotlemfcc  34638  ballotlemsup  34649  tgoldbachgt  34807  bnj545  35037  bnj548  35039  fineqvnttrclse  35268  wevgblacfn  35291  satfv1  35545  trer  36498  filnetlem3  36562  filnetlem4  36563  phpreu  37925  matunitlindflem1  37937  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem26  37967  mblfinlem1  37978  mblfinlem2  37979  mblfinlem3  37980  mblfinlem4  37981  ismblfin  37982  prter1  39325  pmapsub  40214  irrapx1  43256  dfacbasgrp  43536  dgraalem  43573  dgraaub  43576  onexlimgt  43671  cantnftermord  43748  oacl2g  43758  onmcl  43759  omabs2  43760  omcl2  43761  ofoaf  43783  naddwordnexlem3  43827  naddwordnexlem4  43829  brcoffn  44457  clsk3nimkb  44467  clsk1indlem1  44472  dvsconst  44757  dvsid  44758  dvsef  44759  islptre  46049  wallispilem1  46493  fourierdlem52  46586  ovnhoilem1  47029  nprmmul3  47989  gbowgt5  48238  gboge9  48240  nnsum3primesprm  48266  nnsum3primesgbe  48268  bgoldbnnsum3prm  48280  tgoldbachlt  48292  stgrnbgr0  48440  grlicref  48488  gpgedg2ov  48542  pgnbgreunbgr  48601  lincext1  48930  linds0  48941  lindsrng01  48944  lmod1lem3  48965  line2  49228  line2x  49230  inlinecirc02plem  49262  2oppf  49607  setrec1  50166