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  1673  nic-axALT  1674  unidif  4906  iunxdif2  5017  exss  5423  xpiindi  5799  relssres  5993  frpoinsg  6316  nfunsn  6900  exfo  7077  fliftcnv  7286  oprres  7557  f1oweALT  7951  fo1stres  7994  fo2ndres  7995  dftpos3  8223  wfr3g  8298  tfrlem10  8355  odi  8543  omabs  8615  elixpsn  8910  sbthlem2  9052  sbthlem3  9053  fodomr  9092  mapxpen  9107  pssnn  9132  oieu  9492  inf3lem6  9586  frmin  9702  frr3g  9709  djuss  9873  acni3  10000  dfacacn  10095  kmlem1  10104  cflm  10203  cfsuc  10210  hsmexlem2  10380  hsmexlem4  10382  hsmexlem5  10383  axdc3lem4  10406  axcclem  10410  brdom5  10482  brdom4  10483  konigthlem  10521  alephval2  10525  alephmul  10531  wunex3  10694  reclem2pr  11001  suplem2pr  11006  lemulge11  12045  nn0ge2m1nn  12512  0mod  13864  1mod  13865  fzennn  13933  hashbclem  14417  hashge2el2dif  14445  wrdlenge2n0  14517  elovmptnn0wrd  14524  swrdnd  14619  s2f1o  14882  f1oun2prg  14883  cotrtrclfv  14978  resqrex  15216  modfsummods  15759  demoivreALT  16169  pcdiv  16823  prmodvdslcmf  17018  invsym2  17725  oduprs  18261  idghm  19163  gaid  19231  symgsubmefmndALT  19333  subrgid  20482  lbsextlem1  21068  mulgghm2  21386  smadiadet  22557  pmatcollpw3fi  22672  topcld  22922  ntrss  22942  restcld  23059  xkocnv  23701  fbssfi  23724  isfild  23745  alexsublem  23931  alexsubALTlem4  23937  metrest  24412  dscopn  24461  reconnlem1  24715  cphsubrglem  25077  cphipval  25143  itgcnlem  25691  vieta1  26220  jensen  26899  2lgs  27318  nosep1o  27593  nodense  27604  bdayimaon  27605  conway  27711  etasslt  27725  slerec  27731  cofcutr  27832  om2noseqoi  28197  axlowdimlem6  28874  axlowdimlem7  28875  axlowdimlem16  28884  axlowdimlem17  28885  usgr2v1e2w  29179  0edg0rgr  29500  usgr2wlkspthlem2  29688  clwwlkf1  29978  0pthon  30056  ipval2  30636  sspg  30657  ssps  30659  sspmlem  30661  blocni  30734  ubthlem1  30799  bcsiALT  31108  ocsh  31212  chabs2  31446  pjoml6i  31518  osumcor2i  31573  nmopcoi  32024  opsqrlem6  32074  stlei  32169  mdslmd1lem1  32254  mdslmd2i  32259  atcvat3i  32325  atcvat4i  32326  sumdmdlem2  32348  dmdbr5ati  32351  xdivpnfrp  32853  fzo0pmtrlast  33049  tpr2rico  33902  ballotlemfp1  34483  ballotlemfc0  34484  ballotlemfcc  34485  ballotlemsup  34496  tgoldbachgt  34654  bnj545  34885  bnj548  34887  wevgblacfn  35096  satfv1  35350  trer  36304  filnetlem3  36368  filnetlem4  36369  phpreu  37598  matunitlindflem1  37610  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem26  37640  mblfinlem1  37651  mblfinlem2  37652  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  prter1  38872  pmapsub  39762  irrapx1  42816  dfacbasgrp  43097  dgraalem  43134  dgraaub  43137  onexlimgt  43232  cantnftermord  43309  oacl2g  43319  onmcl  43320  omabs2  43321  omcl2  43322  ofoaf  43344  naddwordnexlem3  43388  naddwordnexlem4  43390  brcoffn  44019  clsk3nimkb  44029  clsk1indlem1  44034  dvsconst  44319  dvsid  44320  dvsef  44321  islptre  45617  wallispilem1  46063  fourierdlem52  46156  ovnhoilem1  46599  gbowgt5  47763  gboge9  47765  nnsum3primesprm  47791  nnsum3primesgbe  47793  bgoldbnnsum3prm  47805  tgoldbachlt  47817  stgrnbgr0  47963  grlicref  48004  gpgedg2ov  48057  pgnbgreunbgr  48115  lincext1  48443  linds0  48454  lindsrng01  48457  lmod1lem3  48478  line2  48741  line2x  48743  inlinecirc02plem  48775  2oppf  49121  setrec1  49680