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  1670  nic-axALT  1671  unidif  4947  iunxdif2  5058  exss  5474  xpiindi  5849  relssres  6042  frpoinsg  6366  nfunsn  6949  exfo  7125  fliftcnv  7331  oprres  7601  f1oweALT  7996  fo1stres  8039  fo2ndres  8040  dftpos3  8268  wfr3g  8346  tfrlem10  8426  odi  8616  omabs  8688  elixpsn  8976  sbthlem2  9123  sbthlem3  9124  fodomr  9167  mapxpen  9182  pssnn  9207  phplem2OLD  9253  oieu  9577  inf3lem6  9671  frmin  9787  frr3g  9794  djuss  9958  acni3  10085  dfacacn  10180  kmlem1  10189  cflm  10288  cfsuc  10295  hsmexlem2  10465  hsmexlem4  10467  hsmexlem5  10468  axdc3lem4  10491  axcclem  10495  brdom5  10567  brdom4  10568  konigthlem  10606  alephval2  10610  alephmul  10616  wunex3  10779  reclem2pr  11086  suplem2pr  11091  lemulge11  12128  nn0ge2m1nn  12594  0mod  13939  1mod  13940  fzennn  14006  hashbclem  14488  hashge2el2dif  14516  wrdlenge2n0  14587  elovmptnn0wrd  14594  swrdnd  14689  s2f1o  14952  f1oun2prg  14953  cotrtrclfv  15048  resqrex  15286  modfsummods  15826  demoivreALT  16234  pcdiv  16886  prmodvdslcmf  17081  invsym2  17811  oduprs  18358  idghm  19262  gaid  19330  symgsubmefmndALT  19436  subrgid  20590  lbsextlem1  21178  mulgghm2  21505  smadiadet  22692  pmatcollpw3fi  22807  topcld  23059  ntrss  23079  restcld  23196  xkocnv  23838  fbssfi  23861  isfild  23882  alexsublem  24068  alexsubALTlem4  24074  metrest  24553  dscopn  24602  reconnlem1  24862  cphsubrglem  25225  cphipval  25291  itgcnlem  25840  vieta1  26369  jensen  27047  2lgs  27466  nosep1o  27741  nodense  27752  bdayimaon  27753  conway  27859  etasslt  27873  slerec  27879  cofcutr  27973  om2noseqoi  28324  axlowdimlem6  28977  axlowdimlem7  28978  axlowdimlem16  28987  axlowdimlem17  28988  usgr2v1e2w  29284  0edg0rgr  29605  usgr2wlkspthlem2  29791  clwwlkf1  30078  0pthon  30156  ipval2  30736  sspg  30757  ssps  30759  sspmlem  30761  blocni  30834  ubthlem1  30899  bcsiALT  31208  ocsh  31312  chabs2  31546  pjoml6i  31618  osumcor2i  31673  nmopcoi  32124  opsqrlem6  32174  stlei  32269  mdslmd1lem1  32354  mdslmd2i  32359  atcvat3i  32425  atcvat4i  32426  sumdmdlem2  32448  dmdbr5ati  32451  xdivpnfrp  32900  fzo0pmtrlast  33095  tpr2rico  33873  ballotlemfp1  34473  ballotlemfc0  34474  ballotlemfcc  34475  ballotlemsup  34486  tgoldbachgt  34657  bnj545  34888  bnj548  34890  wevgblacfn  35093  satfv1  35348  trer  36299  filnetlem3  36363  filnetlem4  36364  phpreu  37591  matunitlindflem1  37603  poimirlem16  37623  poimirlem17  37624  poimirlem19  37626  poimirlem20  37627  poimirlem26  37633  mblfinlem1  37644  mblfinlem2  37645  mblfinlem3  37646  mblfinlem4  37647  ismblfin  37648  prter1  38861  pmapsub  39751  2xp3dxp2ge1d  42223  irrapx1  42816  dfacbasgrp  43097  dgraalem  43134  dgraaub  43137  onexlimgt  43232  cantnftermord  43310  oacl2g  43320  onmcl  43321  omabs2  43322  omcl2  43323  ofoaf  43345  naddwordnexlem3  43389  naddwordnexlem4  43391  brcoffn  44020  clsk3nimkb  44030  clsk1indlem1  44035  dvsconst  44326  dvsid  44327  dvsef  44328  islptre  45575  wallispilem1  46021  fourierdlem52  46114  ovnhoilem1  46557  gbowgt5  47687  gboge9  47689  nnsum3primesprm  47715  nnsum3primesgbe  47717  bgoldbnnsum3prm  47729  tgoldbachlt  47741  stgrnbgr0  47867  grlicref  47908  lincext1  48300  linds0  48311  lindsrng01  48314  lmod1lem3  48335  line2  48602  line2x  48604  inlinecirc02plem  48636  setrec1  48922