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  1674  nic-axALT  1675  unidif  4895  iunxdif2  5006  exss  5408  xpiindi  5781  relssres  5977  frpoinsg  6297  nfunsn  6869  exfo  7046  fliftcnv  7253  oprres  7522  f1oweALT  7912  fo1stres  7955  fo2ndres  7956  dftpos3  8182  wfr3g  8257  tfrlem10  8314  odi  8502  omabs  8574  elixpsn  8869  sbthlem2  9010  sbthlem3  9011  fodomr  9050  mapxpen  9065  pssnn  9087  oieu  9434  inf3lem6  9532  frmin  9651  frr3g  9658  djuss  9822  acni3  9947  dfacacn  10042  kmlem1  10051  cflm  10150  cfsuc  10157  hsmexlem2  10327  hsmexlem4  10329  hsmexlem5  10330  axdc3lem4  10353  axcclem  10357  brdom5  10429  brdom4  10430  konigthlem  10468  alephval2  10472  alephmul  10478  wunex3  10641  reclem2pr  10948  suplem2pr  10953  lemulge11  11993  nn0ge2m1nn  12460  0mod  13810  1mod  13811  fzennn  13879  hashbclem  14363  hashge2el2dif  14391  wrdlenge2n0  14463  elovmptnn0wrd  14470  swrdnd  14566  s2f1o  14827  f1oun2prg  14828  cotrtrclfv  14923  resqrex  15161  modfsummods  15704  demoivreALT  16114  pcdiv  16768  prmodvdslcmf  16963  invsym2  17674  oduprs  18210  chnexg  18528  idghm  19147  gaid  19215  symgsubmefmndALT  19319  subrgid  20492  lbsextlem1  21099  mulgghm2  21417  smadiadet  22588  pmatcollpw3fi  22703  topcld  22953  ntrss  22973  restcld  23090  xkocnv  23732  fbssfi  23755  isfild  23776  alexsublem  23962  alexsubALTlem4  23968  metrest  24442  dscopn  24491  reconnlem1  24745  cphsubrglem  25107  cphipval  25173  itgcnlem  25721  vieta1  26250  jensen  26929  2lgs  27348  nosep1o  27623  nodense  27634  bdayimaon  27635  conway  27743  etasslt  27757  slerec  27763  cofcutr  27871  om2noseqoi  28236  axlowdimlem6  28929  axlowdimlem7  28930  axlowdimlem16  28939  axlowdimlem17  28940  usgr2v1e2w  29234  0edg0rgr  29555  usgr2wlkspthlem2  29740  clwwlkf1  30033  0pthon  30111  ipval2  30691  sspg  30712  ssps  30714  sspmlem  30716  blocni  30789  ubthlem1  30854  bcsiALT  31163  ocsh  31267  chabs2  31501  pjoml6i  31573  osumcor2i  31628  nmopcoi  32079  opsqrlem6  32129  stlei  32224  mdslmd1lem1  32309  mdslmd2i  32314  atcvat3i  32380  atcvat4i  32381  sumdmdlem2  32403  dmdbr5ati  32406  xdivpnfrp  32922  fzo0pmtrlast  33070  tpr2rico  33948  ballotlemfp1  34528  ballotlemfc0  34529  ballotlemfcc  34530  ballotlemsup  34541  tgoldbachgt  34699  bnj545  34930  bnj548  34932  fineqvnttrclse  35167  wevgblacfn  35176  satfv1  35430  trer  36383  filnetlem3  36447  filnetlem4  36448  phpreu  37667  matunitlindflem1  37679  poimirlem16  37699  poimirlem17  37700  poimirlem19  37702  poimirlem20  37703  poimirlem26  37709  mblfinlem1  37720  mblfinlem2  37721  mblfinlem3  37722  mblfinlem4  37723  ismblfin  37724  prter1  39001  pmapsub  39890  irrapx1  42948  dfacbasgrp  43228  dgraalem  43265  dgraaub  43268  onexlimgt  43363  cantnftermord  43440  oacl2g  43450  onmcl  43451  omabs2  43452  omcl2  43453  ofoaf  43475  naddwordnexlem3  43519  naddwordnexlem4  43521  brcoffn  44150  clsk3nimkb  44160  clsk1indlem1  44165  dvsconst  44450  dvsid  44451  dvsef  44452  islptre  45746  wallispilem1  46190  fourierdlem52  46283  ovnhoilem1  46726  gbowgt5  47889  gboge9  47891  nnsum3primesprm  47917  nnsum3primesgbe  47919  bgoldbnnsum3prm  47931  tgoldbachlt  47943  stgrnbgr0  48091  grlicref  48139  gpgedg2ov  48193  pgnbgreunbgr  48252  lincext1  48582  linds0  48593  lindsrng01  48596  lmod1lem3  48617  line2  48880  line2x  48882  inlinecirc02plem  48914  2oppf  49260  setrec1  49819