Theorem jctil 522

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 514	1 ⊢ (𝜑 → (𝜒 ∧ 𝜓))

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  jctl  526  nic-ax  1673  nic-axALT  1674  unidif  4875  iunxdif2  4980  exss  5358  xpiindi  5709  relssres  5896  nfunsn  6710  exfo  6874  fliftcnv  7067  oprres  7319  f1oweALT  7676  fo1stres  7718  fo2ndres  7719  dftpos3  7913  wfr3g  7956  tfrlem10  8026  odi  8208  omabs  8277  elixpsn  8504  sbthlem2  8631  sbthlem3  8632  fodomr  8671  mapxpen  8686  phplem2  8700  pssnn  8739  oieu  9006  inf3lem6  9099  djuss  9352  acni3  9476  dfacacn  9570  kmlem1  9579  cflm  9675  cfsuc  9682  hsmexlem2  9852  hsmexlem4  9854  hsmexlem5  9855  axdc3lem4  9878  axcclem  9882  brdom5  9954  brdom4  9955  konigthlem  9993  alephval2  9997  alephmul  10003  wunex3  10166  reclem2pr  10473  suplem2pr  10478  lemulge11  11505  nn0ge2m1nn  11967  0mod  13273  1mod  13274  fzennn  13339  hashbclem  13813  hashge2el2dif  13841  wrdlenge2n0  13907  elovmptnn0wrd  13914  swrdnd  14019  s2f1o  14281  f1oun2prg  14282  cotrtrclfv  14375  resqrex  14613  modfsummods  15151  demoivreALT  15557  pcdiv  16192  prmodvdslcmf  16386  invsym2  17036  idghm  18376  gaid  18432  symgsubmefmndALT  18534  subrgid  19540  lbsextlem1  19933  mulgghm2  20647  smadiadet  21282  pmatcollpw3fi  21396  topcld  21646  ntrss  21666  restcld  21783  xkocnv  22425  fbssfi  22448  isfild  22469  alexsublem  22655  alexsubALTlem4  22661  metrest  23137  dscopn  23186  reconnlem1  23437  cphsubrglem  23784  cphipval  23849  itgcnlem  24393  vieta1  24904  jensen  25569  2lgs  25986  axlowdimlem6  26736  axlowdimlem7  26737  axlowdimlem16  26746  axlowdimlem17  26747  usgr2v1e2w  27037  0edg0rgr  27357  usgr2wlkspthlem2  27542  clwwlkf1  27831  0pthon  27909  ipval2  28487  sspg  28508  ssps  28510  sspmlem  28512  blocni  28585  ubthlem1  28650  bcsiALT  28959  ocsh  29063  chabs2  29297  pjoml6i  29369  osumcor2i  29424  nmopcoi  29875  opsqrlem6  29925  stlei  30020  mdslmd1lem1  30105  mdslmd2i  30110  atcvat3i  30176  atcvat4i  30177  sumdmdlem2  30199  dmdbr5ati  30202  xdivpnfrp  30613  oduprs  30647  tpr2rico  31159  ballotlemfp1  31753  ballotlemfc0  31754  ballotlemfcc  31755  ballotlemsup  31766  tgoldbachgt  31938  bnj545  32171  bnj548  32173  satfv1  32614  frpoinsg  33085  frr3g  33125  nosep1o  33190  nodense  33200  bdayimaon  33201  nulsslt  33266  conway  33268  etasslt  33278  slerec  33281  trer  33668  filnetlem3  33732  filnetlem4  33733  phpreu  34880  matunitlindflem1  34892  poimirlem16  34912  poimirlem17  34913  poimirlem19  34915  poimirlem20  34916  poimirlem26  34922  mblfinlem1  34933  mblfinlem2  34934  mblfinlem3  34935  mblfinlem4  34936  ismblfin  34937  prter1  36019  pmapsub  36908  irrapx1  39431  dfacbasgrp  39714  dgraalem  39751  dgraaub  39754  brcoffn  40386  clsk3nimkb  40396  clsk1indlem1  40401  dvsconst  40668  dvsid  40669  dvsef  40670  islptre  41906  wallispilem1  42357  fourierdlem52  42450  ovnhoilem1  42890  gbowgt5  43934  gboge9  43936  nnsum3primesprm  43962  nnsum3primesgbe  43964  bgoldbnnsum3prm  43976  tgoldbachlt  43988  lincext1  44516  linds0  44527  lindsrng01  44530  lmod1lem3  44551  line2  44746  line2x  44748  inlinecirc02plem  44780  setrec1  44801