Theorem jctil 527

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  jctl  531  nic-ax  1692  nic-axALT  1693  unidif  4898  iunxdif2  5008  exss  5427  xpiindi  5803  relssres  6004  frpoinsg  6324  nfunsn  6900  exfo  7080  fliftcnv  7289  oprres  7558  f1oweALT  7947  fo1stres  7990  fo2ndres  7991  dftpos3  8217  wfr3g  8293  tfrlem10  8351  odi  8541  omabs  8614  elixpsn  8912  sbthlem2  9053  sbthlem3  9054  fodomr  9093  mapxpen  9108  pssnn  9130  oieu  9480  inf3lem6  9581  frmin  9700  frr3g  9707  djuss  9871  acni3  9996  dfacacn  10091  kmlem1  10100  cflm  10199  cfsuc  10207  hsmexlem2  10377  hsmexlem4  10379  hsmexlem5  10380  axdc3lem4  10403  axcclem  10407  brdom5  10479  brdom4  10480  konigthlem  10519  alephval2  10523  alephmul  10529  wunex3  10692  reclem2pr  10999  suplem2pr  11004  lemulge11  12047  nn0ge2m1nn  12544  0mod  13905  1mod  13906  fzennn  13974  hashbclem  14458  hashge2el2dif  14486  wrdlenge2n0  14558  elovmptnn0wrd  14565  swrdnd  14661  s2f1o  14922  f1oun2prg  14923  cotrtrclfv  15018  resqrex  15267  modfsummods  15811  demoivreALT  16223  pcdiv  16878  prmodvdslcmf  17073  invsym2  17786  oduprs  18322  chnexg  18640  idghm  19261  gaid  19329  symgsubmefmndALT  19433  subrgid  20609  lbsextlem1  21215  mulgghm2  21515  smadiadet  22717  pmatcollpw3fi  22832  topcld  23082  ntrss  23102  restcld  23219  xkocnv  23861  fbssfi  23884  isfild  23905  alexsublem  24091  alexsubALTlem4  24097  metrest  24571  dscopn  24620  reconnlem1  24874  cphsubrglem  25226  cphipval  25292  itgcnlem  25839  vieta1  26363  jensen  27040  2lgs  27458  nosep1o  27732  nodense  27743  bdayimaon  27744  conway  27859  etaslts  27873  lesrec  27879  cofcutr  28004  om2noseqoi  28383  axlowdimlem6  29104  axlowdimlem7  29105  axlowdimlem16  29114  axlowdimlem17  29115  usgr2v1e2w  29409  0edg0rgr  29729  usgr2wlkspthlem2  29914  clwwlkf1  30207  0pthon  30285  ipval2  30866  sspg  30887  ssps  30889  sspmlem  30891  blocni  30964  ubthlem1  31029  bcsiALT  31338  ocsh  31442  chabs2  31676  pjoml6i  31748  osumcor2i  31803  nmopcoi  32254  opsqrlem6  32304  stlei  32399  mdslmd1lem1  32484  mdslmd2i  32489  atcvat3i  32555  atcvat4i  32556  sumdmdlem2  32578  dmdbr5ati  32581  xdivpnfrp  33070  fzo0pmtrlast  33232  tpr2rico  34169  ballotlemfp1  34749  ballotlemfc0  34750  ballotlemfcc  34751  ballotlemsup  34762  tgoldbachgt  34917  bnj545  35150  bnj548  35152  fineqvnttrclse  35380  wevgblacfn  35414  satfv1  35673  trer  36636  filnetlem3  36700  filnetlem4  36701  phpreu  38063  matunitlindflem1  38075  poimirlem16  38095  poimirlem17  38096  poimirlem19  38098  poimirlem20  38099  poimirlem26  38105  mblfinlem1  38116  mblfinlem2  38117  mblfinlem3  38118  mblfinlem4  38119  ismblfin  38120  prter1  39463  pmapsub  40352  irrapx1  43365  dfacbasgrp  43645  dgraalem  43682  dgraaub  43685  onexlimgt  43780  cantnftermord  43857  oacl2g  43867  onmcl  43868  omabs2  43869  omcl2  43870  ofoaf  43892  naddwordnexlem3  43936  naddwordnexlem4  43938  brcoffn  44566  clsk3nimkb  44576  clsk1indlem1  44581  dvsconst  44866  dvsid  44867  dvsef  44868  islptre  46155  wallispilem1  46599  fourierdlem52  46692  ovnhoilem1  47135  nprmmul3  48095  gbowgt5  48344  gboge9  48346  nnsum3primesprm  48372  nnsum3primesgbe  48374  bgoldbnnsum3prm  48386  tgoldbachlt  48398  stgrnbgr0  48546  grlicref  48594  gpgedg2ov  48648  pgnbgreunbgr  48707  lincext1  49036  linds0  49047  lindsrng01  49050  lmod1lem3  49071  line2  49334  line2x  49336  inlinecirc02plem  49368  2oppf  49713  setrec1  50272