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  1672  nic-axALT  1673  unidif  4941  iunxdif2  5052  exss  5467  xpiindi  5845  relssres  6039  frpoinsg  6363  nfunsn  6947  exfo  7124  fliftcnv  7332  oprres  7602  f1oweALT  7998  fo1stres  8041  fo2ndres  8042  dftpos3  8270  wfr3g  8348  tfrlem10  8428  odi  8618  omabs  8690  elixpsn  8978  sbthlem2  9125  sbthlem3  9126  fodomr  9169  mapxpen  9184  pssnn  9209  phplem2OLD  9256  oieu  9580  inf3lem6  9674  frmin  9790  frr3g  9797  djuss  9961  acni3  10088  dfacacn  10183  kmlem1  10192  cflm  10291  cfsuc  10298  hsmexlem2  10468  hsmexlem4  10470  hsmexlem5  10471  axdc3lem4  10494  axcclem  10498  brdom5  10570  brdom4  10571  konigthlem  10609  alephval2  10613  alephmul  10619  wunex3  10782  reclem2pr  11089  suplem2pr  11094  lemulge11  12131  nn0ge2m1nn  12598  0mod  13943  1mod  13944  fzennn  14010  hashbclem  14492  hashge2el2dif  14520  wrdlenge2n0  14591  elovmptnn0wrd  14598  swrdnd  14693  s2f1o  14956  f1oun2prg  14957  cotrtrclfv  15052  resqrex  15290  modfsummods  15830  demoivreALT  16238  pcdiv  16891  prmodvdslcmf  17086  invsym2  17808  oduprs  18347  idghm  19250  gaid  19318  symgsubmefmndALT  19422  subrgid  20574  lbsextlem1  21161  mulgghm2  21488  smadiadet  22677  pmatcollpw3fi  22792  topcld  23044  ntrss  23064  restcld  23181  xkocnv  23823  fbssfi  23846  isfild  23867  alexsublem  24053  alexsubALTlem4  24059  metrest  24538  dscopn  24587  reconnlem1  24849  cphsubrglem  25212  cphipval  25278  itgcnlem  25826  vieta1  26355  jensen  27033  2lgs  27452  nosep1o  27727  nodense  27738  bdayimaon  27739  conway  27845  etasslt  27859  slerec  27865  cofcutr  27959  om2noseqoi  28310  axlowdimlem6  28963  axlowdimlem7  28964  axlowdimlem16  28973  axlowdimlem17  28974  usgr2v1e2w  29270  0edg0rgr  29591  usgr2wlkspthlem2  29779  clwwlkf1  30069  0pthon  30147  ipval2  30727  sspg  30748  ssps  30750  sspmlem  30752  blocni  30825  ubthlem1  30890  bcsiALT  31199  ocsh  31303  chabs2  31537  pjoml6i  31609  osumcor2i  31664  nmopcoi  32115  opsqrlem6  32165  stlei  32260  mdslmd1lem1  32345  mdslmd2i  32350  atcvat3i  32416  atcvat4i  32417  sumdmdlem2  32439  dmdbr5ati  32442  xdivpnfrp  32916  fzo0pmtrlast  33113  tpr2rico  33912  ballotlemfp1  34495  ballotlemfc0  34496  ballotlemfcc  34497  ballotlemsup  34508  tgoldbachgt  34679  bnj545  34910  bnj548  34912  wevgblacfn  35115  satfv1  35369  trer  36318  filnetlem3  36382  filnetlem4  36383  phpreu  37612  matunitlindflem1  37624  poimirlem16  37644  poimirlem17  37645  poimirlem19  37647  poimirlem20  37648  poimirlem26  37654  mblfinlem1  37665  mblfinlem2  37666  mblfinlem3  37667  mblfinlem4  37668  ismblfin  37669  prter1  38881  pmapsub  39771  2xp3dxp2ge1d  42243  irrapx1  42844  dfacbasgrp  43125  dgraalem  43162  dgraaub  43165  onexlimgt  43260  cantnftermord  43338  oacl2g  43348  onmcl  43349  omabs2  43350  omcl2  43351  ofoaf  43373  naddwordnexlem3  43417  naddwordnexlem4  43419  brcoffn  44048  clsk3nimkb  44058  clsk1indlem1  44063  dvsconst  44354  dvsid  44355  dvsef  44356  islptre  45639  wallispilem1  46085  fourierdlem52  46178  ovnhoilem1  46621  gbowgt5  47754  gboge9  47756  nnsum3primesprm  47782  nnsum3primesgbe  47784  bgoldbnnsum3prm  47796  tgoldbachlt  47808  stgrnbgr0  47936  grlicref  47977  lincext1  48376  linds0  48387  lindsrng01  48390  lmod1lem3  48411  line2  48678  line2x  48680  inlinecirc02plem  48712  setrec1  49265