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  4895  iunxdif2  5005  exss  5410  xpiindi  5782  relssres  5977  frpoinsg  6295  nfunsn  6866  exfo  7043  fliftcnv  7252  oprres  7521  f1oweALT  7914  fo1stres  7957  fo2ndres  7958  dftpos3  8184  wfr3g  8259  tfrlem10  8316  odi  8504  omabs  8576  elixpsn  8871  sbthlem2  9012  sbthlem3  9013  fodomr  9052  mapxpen  9067  pssnn  9092  oieu  9450  inf3lem6  9548  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  10481  alephval2  10485  alephmul  10491  wunex3  10654  reclem2pr  10961  suplem2pr  10966  lemulge11  12005  nn0ge2m1nn  12472  0mod  13824  1mod  13825  fzennn  13893  hashbclem  14377  hashge2el2dif  14405  wrdlenge2n0  14477  elovmptnn0wrd  14484  swrdnd  14579  s2f1o  14841  f1oun2prg  14842  cotrtrclfv  14937  resqrex  15175  modfsummods  15718  demoivreALT  16128  pcdiv  16782  prmodvdslcmf  16977  invsym2  17688  oduprs  18224  idghm  19128  gaid  19196  symgsubmefmndALT  19300  subrgid  20476  lbsextlem1  21083  mulgghm2  21401  smadiadet  22573  pmatcollpw3fi  22688  topcld  22938  ntrss  22958  restcld  23075  xkocnv  23717  fbssfi  23740  isfild  23761  alexsublem  23947  alexsubALTlem4  23953  metrest  24428  dscopn  24477  reconnlem1  24731  cphsubrglem  25093  cphipval  25159  itgcnlem  25707  vieta1  26236  jensen  26915  2lgs  27334  nosep1o  27609  nodense  27620  bdayimaon  27621  conway  27728  etasslt  27742  slerec  27748  cofcutr  27855  om2noseqoi  28220  axlowdimlem6  28910  axlowdimlem7  28911  axlowdimlem16  28920  axlowdimlem17  28921  usgr2v1e2w  29215  0edg0rgr  29536  usgr2wlkspthlem2  29721  clwwlkf1  30011  0pthon  30089  ipval2  30669  sspg  30690  ssps  30692  sspmlem  30694  blocni  30767  ubthlem1  30832  bcsiALT  31141  ocsh  31245  chabs2  31479  pjoml6i  31551  osumcor2i  31606  nmopcoi  32057  opsqrlem6  32107  stlei  32202  mdslmd1lem1  32287  mdslmd2i  32292  atcvat3i  32358  atcvat4i  32359  sumdmdlem2  32381  dmdbr5ati  32384  xdivpnfrp  32886  fzo0pmtrlast  33047  tpr2rico  33881  ballotlemfp1  34462  ballotlemfc0  34463  ballotlemfcc  34464  ballotlemsup  34475  tgoldbachgt  34633  bnj545  34864  bnj548  34866  wevgblacfn  35084  satfv1  35338  trer  36292  filnetlem3  36356  filnetlem4  36357  phpreu  37586  matunitlindflem1  37598  poimirlem16  37618  poimirlem17  37619  poimirlem19  37621  poimirlem20  37622  poimirlem26  37628  mblfinlem1  37639  mblfinlem2  37640  mblfinlem3  37641  mblfinlem4  37642  ismblfin  37643  prter1  38860  pmapsub  39750  irrapx1  42804  dfacbasgrp  43084  dgraalem  43121  dgraaub  43124  onexlimgt  43219  cantnftermord  43296  oacl2g  43306  onmcl  43307  omabs2  43308  omcl2  43309  ofoaf  43331  naddwordnexlem3  43375  naddwordnexlem4  43377  brcoffn  44006  clsk3nimkb  44016  clsk1indlem1  44021  dvsconst  44306  dvsid  44307  dvsef  44308  islptre  45604  wallispilem1  46050  fourierdlem52  46143  ovnhoilem1  46586  gbowgt5  47750  gboge9  47752  nnsum3primesprm  47778  nnsum3primesgbe  47780  bgoldbnnsum3prm  47792  tgoldbachlt  47804  stgrnbgr0  47952  grlicref  48000  gpgedg2ov  48054  pgnbgreunbgr  48113  lincext1  48443  linds0  48454  lindsrng01  48457  lmod1lem3  48478  line2  48741  line2x  48743  inlinecirc02plem  48775  2oppf  49121  setrec1  49680