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  4886  iunxdif2  4997  exss  5410  xpiindi  5784  relssres  5981  frpoinsg  6301  nfunsn  6873  exfo  7051  fliftcnv  7259  oprres  7528  f1oweALT  7918  fo1stres  7961  fo2ndres  7962  dftpos3  8187  wfr3g  8262  tfrlem10  8319  odi  8507  omabs  8580  elixpsn  8878  sbthlem2  9019  sbthlem3  9020  fodomr  9059  mapxpen  9074  pssnn  9096  oieu  9447  inf3lem6  9545  frmin  9664  frr3g  9671  djuss  9835  acni3  9960  dfacacn  10055  kmlem1  10064  cflm  10163  cfsuc  10170  hsmexlem2  10340  hsmexlem4  10342  hsmexlem5  10343  axdc3lem4  10366  axcclem  10370  brdom5  10442  brdom4  10443  konigthlem  10482  alephval2  10486  alephmul  10492  wunex3  10655  reclem2pr  10962  suplem2pr  10967  lemulge11  12009  nn0ge2m1nn  12498  0mod  13852  1mod  13853  fzennn  13921  hashbclem  14405  hashge2el2dif  14433  wrdlenge2n0  14505  elovmptnn0wrd  14512  swrdnd  14608  s2f1o  14869  f1oun2prg  14870  cotrtrclfv  14965  resqrex  15203  modfsummods  15747  demoivreALT  16159  pcdiv  16814  prmodvdslcmf  17009  invsym2  17721  oduprs  18257  chnexg  18575  idghm  19197  gaid  19265  symgsubmefmndALT  19369  subrgid  20541  lbsextlem1  21148  mulgghm2  21466  smadiadet  22645  pmatcollpw3fi  22760  topcld  23010  ntrss  23030  restcld  23147  xkocnv  23789  fbssfi  23812  isfild  23833  alexsublem  24019  alexsubALTlem4  24025  metrest  24499  dscopn  24548  reconnlem1  24802  cphsubrglem  25154  cphipval  25220  itgcnlem  25767  vieta1  26289  jensen  26966  2lgs  27384  nosep1o  27659  nodense  27670  bdayimaon  27671  conway  27785  etaslts  27799  lesrec  27805  cofcutr  27930  om2noseqoi  28309  axlowdimlem6  29030  axlowdimlem7  29031  axlowdimlem16  29040  axlowdimlem17  29041  usgr2v1e2w  29335  0edg0rgr  29656  usgr2wlkspthlem2  29841  clwwlkf1  30134  0pthon  30212  ipval2  30793  sspg  30814  ssps  30816  sspmlem  30818  blocni  30891  ubthlem1  30956  bcsiALT  31265  ocsh  31369  chabs2  31603  pjoml6i  31675  osumcor2i  31730  nmopcoi  32181  opsqrlem6  32231  stlei  32326  mdslmd1lem1  32411  mdslmd2i  32416  atcvat3i  32482  atcvat4i  32483  sumdmdlem2  32505  dmdbr5ati  32508  xdivpnfrp  33007  fzo0pmtrlast  33168  tpr2rico  34072  ballotlemfp1  34652  ballotlemfc0  34653  ballotlemfcc  34654  ballotlemsup  34665  tgoldbachgt  34823  bnj545  35053  bnj548  35055  fineqvnttrclse  35284  wevgblacfn  35307  satfv1  35561  trer  36514  filnetlem3  36578  filnetlem4  36579  phpreu  37939  matunitlindflem1  37951  poimirlem16  37971  poimirlem17  37972  poimirlem19  37974  poimirlem20  37975  poimirlem26  37981  mblfinlem1  37992  mblfinlem2  37993  mblfinlem3  37994  mblfinlem4  37995  ismblfin  37996  prter1  39339  pmapsub  40228  irrapx1  43274  dfacbasgrp  43554  dgraalem  43591  dgraaub  43594  onexlimgt  43689  cantnftermord  43766  oacl2g  43776  onmcl  43777  omabs2  43778  omcl2  43779  ofoaf  43801  naddwordnexlem3  43845  naddwordnexlem4  43847  brcoffn  44475  clsk3nimkb  44485  clsk1indlem1  44490  dvsconst  44775  dvsid  44776  dvsef  44777  islptre  46067  wallispilem1  46511  fourierdlem52  46604  ovnhoilem1  47047  nprmmul3  48001  gbowgt5  48250  gboge9  48252  nnsum3primesprm  48278  nnsum3primesgbe  48280  bgoldbnnsum3prm  48292  tgoldbachlt  48304  stgrnbgr0  48452  grlicref  48500  gpgedg2ov  48554  pgnbgreunbgr  48613  lincext1  48942  linds0  48953  lindsrng01  48956  lmod1lem3  48977  line2  49240  line2x  49242  inlinecirc02plem  49274  2oppf  49619  setrec1  50178