Theorem jctil 512

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

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  jctl  516  nic-ax  1637  nic-axALT  1638  unidif  4742  iunxdif2  4840  exss  5209  xpiindi  5553  relssres  5736  nfunsn  6535  exfo  6693  fliftcnv  6886  oprres  7131  f1oweALT  7484  fo1stres  7526  fo2ndres  7527  dftpos3  7712  wfr3g  7755  tfrlem10  7826  odi  8005  omabs  8073  elixpsn  8297  sbthlem2  8423  sbthlem3  8424  fodomr  8463  mapxpen  8478  phplem2  8492  pssnn  8530  oieu  8797  inf3lem6  8889  djuss  9142  acni3  9266  dfacacn  9360  kmlem1  9369  cflm  9469  cfsuc  9476  hsmexlem2  9646  hsmexlem4  9648  hsmexlem5  9649  axdc3lem4  9672  axcclem  9676  brdom5  9748  brdom4  9749  konigthlem  9787  alephval2  9791  alephmul  9797  wunex3  9960  reclem2pr  10267  suplem2pr  10272  lemulge11  11302  nn0ge2m1nn  11775  0mod  13084  1mod  13085  fzennn  13150  hashbclem  13622  hashge2el2dif  13648  wrdlenge2n0  13714  elovmptnn0wrd  13721  swrdnd  13821  2swrdeqwrdeqOLD  13845  s2f1o  14139  f1oun2prg  14140  cotrtrclfv  14232  resqrex  14470  modfsummods  15007  demoivreALT  15413  pcdiv  16044  prmodvdslcmf  16238  invsym2  16904  idghm  18157  gaid  18213  subrgid  19273  lbsextlem1  19665  mulgghm2  20362  smadiadet  20999  pmatcollpw3fi  21113  topcld  21363  ntrss  21383  restcld  21500  xkocnv  22142  fbssfi  22165  isfild  22186  alexsublem  22372  alexsubALTlem4  22378  metrest  22853  dscopn  22902  reconnlem1  23153  cphsubrglem  23500  cphipval  23565  itgcnlem  24109  vieta1  24620  jensen  25284  2lgs  25701  axlowdimlem6  26452  axlowdimlem7  26453  axlowdimlem16  26462  axlowdimlem17  26463  usgr2v1e2w  26753  0edg0rgr  27073  usgr2wlkspthlem2  27263  clwwlkf1OLD  27582  clwwlkf1  27587  0pthon  27672  ipval2  28277  sspg  28298  ssps  28300  sspmlem  28302  blocni  28375  ubthlem1  28441  bcsiALT  28751  ocsh  28857  chabs2  29091  pjoml6i  29163  osumcor2i  29218  nmopcoi  29669  opsqrlem6  29719  stlei  29814  mdslmd1lem1  29899  mdslmd2i  29904  atcvat3i  29970  atcvat4i  29971  sumdmdlem2  29993  dmdbr5ati  29996  xdivpnfrp  30380  oduprs  30402  tpr2rico  30832  ballotlemfp1  31428  ballotlemfc0  31429  ballotlemfcc  31430  ballotlemsup  31441  tgoldbachgt  31615  bnj545  31847  bnj548  31849  frpoinsg  32635  frr3g  32675  nosep1o  32740  nodense  32750  bdayimaon  32751  nulsslt  32816  conway  32818  etasslt  32828  slerec  32831  trer  33218  filnetlem3  33282  filnetlem4  33283  phpreu  34350  matunitlindflem1  34362  poimirlem16  34382  poimirlem17  34383  poimirlem19  34385  poimirlem20  34386  poimirlem26  34392  mblfinlem1  34403  mblfinlem2  34404  mblfinlem3  34405  mblfinlem4  34406  ismblfin  34407  prter1  35493  pmapsub  36382  irrapx1  38855  dfacbasgrp  39138  dgraalem  39175  dgraaub  39178  brcoffn  39777  clsk3nimkb  39787  clsk1indlem1  39792  dvsconst  40112  dvsid  40113  dvsef  40114  islptre  41361  wallispilem1  41811  fourierdlem52  41904  ovnhoilem1  42344  gbowgt5  43325  gboge9  43327  nnsum3primesprm  43353  nnsum3primesgbe  43355  bgoldbnnsum3prm  43367  tgoldbachlt  43379  lincext1  43906  linds0  43917  lindsrng01  43920  lmod1lem3  43941  line2  44137  line2x  44139  inlinecirc02plem  44171  setrec1  44191