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  1671  nic-axALT  1672  unidif  4966  iunxdif2  5076  exss  5483  xpiindi  5860  relssres  6051  frpoinsg  6375  nfunsn  6962  exfo  7139  fliftcnv  7347  oprres  7618  f1oweALT  8013  fo1stres  8056  fo2ndres  8057  dftpos3  8285  wfr3g  8363  tfrlem10  8443  odi  8635  omabs  8707  elixpsn  8995  sbthlem2  9150  sbthlem3  9151  fodomr  9194  mapxpen  9209  pssnn  9234  phplem2OLD  9281  oieu  9608  inf3lem6  9702  frmin  9818  frr3g  9825  djuss  9989  acni3  10116  dfacacn  10211  kmlem1  10220  cflm  10319  cfsuc  10326  hsmexlem2  10496  hsmexlem4  10498  hsmexlem5  10499  axdc3lem4  10522  axcclem  10526  brdom5  10598  brdom4  10599  konigthlem  10637  alephval2  10641  alephmul  10647  wunex3  10810  reclem2pr  11117  suplem2pr  11122  lemulge11  12157  nn0ge2m1nn  12622  0mod  13953  1mod  13954  fzennn  14019  hashbclem  14501  hashge2el2dif  14529  wrdlenge2n0  14600  elovmptnn0wrd  14607  swrdnd  14702  s2f1o  14965  f1oun2prg  14966  cotrtrclfv  15061  resqrex  15299  modfsummods  15841  demoivreALT  16249  pcdiv  16899  prmodvdslcmf  17094  invsym2  17824  idghm  19271  gaid  19339  symgsubmefmndALT  19445  subrgid  20601  lbsextlem1  21183  mulgghm2  21510  smadiadet  22697  pmatcollpw3fi  22812  topcld  23064  ntrss  23084  restcld  23201  xkocnv  23843  fbssfi  23866  isfild  23887  alexsublem  24073  alexsubALTlem4  24079  metrest  24558  dscopn  24607  reconnlem1  24867  cphsubrglem  25230  cphipval  25296  itgcnlem  25845  vieta1  26372  jensen  27050  2lgs  27469  nosep1o  27744  nodense  27755  bdayimaon  27756  conway  27862  etasslt  27876  slerec  27882  cofcutr  27976  om2noseqoi  28327  axlowdimlem6  28980  axlowdimlem7  28981  axlowdimlem16  28990  axlowdimlem17  28991  usgr2v1e2w  29287  0edg0rgr  29608  usgr2wlkspthlem2  29794  clwwlkf1  30081  0pthon  30159  ipval2  30739  sspg  30760  ssps  30762  sspmlem  30764  blocni  30837  ubthlem1  30902  bcsiALT  31211  ocsh  31315  chabs2  31549  pjoml6i  31621  osumcor2i  31676  nmopcoi  32127  opsqrlem6  32177  stlei  32272  mdslmd1lem1  32357  mdslmd2i  32362  atcvat3i  32428  atcvat4i  32429  sumdmdlem2  32451  dmdbr5ati  32454  xdivpnfrp  32897  oduprs  32937  fzo0pmtrlast  33085  tpr2rico  33858  ballotlemfp1  34456  ballotlemfc0  34457  ballotlemfcc  34458  ballotlemsup  34469  tgoldbachgt  34640  bnj545  34871  bnj548  34873  wevgblacfn  35076  satfv1  35331  trer  36282  filnetlem3  36346  filnetlem4  36347  phpreu  37564  matunitlindflem1  37576  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem26  37606  mblfinlem1  37617  mblfinlem2  37618  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  prter1  38835  pmapsub  39725  2xp3dxp2ge1d  42198  irrapx1  42784  dfacbasgrp  43065  dgraalem  43102  dgraaub  43105  onexlimgt  43204  cantnftermord  43282  oacl2g  43292  onmcl  43293  omabs2  43294  omcl2  43295  ofoaf  43317  naddwordnexlem3  43361  naddwordnexlem4  43363  brcoffn  43992  clsk3nimkb  44002  clsk1indlem1  44007  dvsconst  44299  dvsid  44300  dvsef  44301  islptre  45540  wallispilem1  45986  fourierdlem52  46079  ovnhoilem1  46522  gbowgt5  47636  gboge9  47638  nnsum3primesprm  47664  nnsum3primesgbe  47666  bgoldbnnsum3prm  47678  tgoldbachlt  47690  grlicref  47829  lincext1  48183  linds0  48194  lindsrng01  48197  lmod1lem3  48218  line2  48486  line2x  48488  inlinecirc02plem  48520  setrec1  48783