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 206  df-an 396

This theorem is referenced by:  jctl  523  nic-ax  1677  nic-axALT  1678  unidif  4872  iunxdif2  4979  exss  5372  xpiindi  5733  relssres  5921  frpoinsg  6231  nfunsn  6793  exfo  6963  fliftcnv  7162  oprres  7418  f1oweALT  7788  fo1stres  7830  fo2ndres  7831  dftpos3  8031  wfr3g  8109  tfrlem10  8189  odi  8372  omabs  8441  elixpsn  8683  sbthlem2  8824  sbthlem3  8825  fodomr  8864  mapxpen  8879  phplem2  8893  pssnn  8913  pssnnOLD  8969  oieu  9228  inf3lem6  9321  frr3g  9445  djuss  9609  acni3  9734  dfacacn  9828  kmlem1  9837  cflm  9937  cfsuc  9944  hsmexlem2  10114  hsmexlem4  10116  hsmexlem5  10117  axdc3lem4  10140  axcclem  10144  brdom5  10216  brdom4  10217  konigthlem  10255  alephval2  10259  alephmul  10265  wunex3  10428  reclem2pr  10735  suplem2pr  10740  lemulge11  11767  nn0ge2m1nn  12232  0mod  13550  1mod  13551  fzennn  13616  hashbclem  14092  hashge2el2dif  14122  wrdlenge2n0  14183  elovmptnn0wrd  14190  swrdnd  14295  s2f1o  14557  f1oun2prg  14558  cotrtrclfv  14651  resqrex  14890  modfsummods  15433  demoivreALT  15838  pcdiv  16481  prmodvdslcmf  16676  invsym2  17392  idghm  18764  gaid  18820  symgsubmefmndALT  18926  subrgid  19941  lbsextlem1  20335  mulgghm2  20610  smadiadet  21727  pmatcollpw3fi  21842  topcld  22094  ntrss  22114  restcld  22231  xkocnv  22873  fbssfi  22896  isfild  22917  alexsublem  23103  alexsubALTlem4  23109  metrest  23586  dscopn  23635  reconnlem1  23895  cphsubrglem  24246  cphipval  24312  itgcnlem  24859  vieta1  25377  jensen  26043  2lgs  26460  axlowdimlem6  27218  axlowdimlem7  27219  axlowdimlem16  27228  axlowdimlem17  27229  usgr2v1e2w  27522  0edg0rgr  27842  usgr2wlkspthlem2  28027  clwwlkf1  28314  0pthon  28392  ipval2  28970  sspg  28991  ssps  28993  sspmlem  28995  blocni  29068  ubthlem1  29133  bcsiALT  29442  ocsh  29546  chabs2  29780  pjoml6i  29852  osumcor2i  29907  nmopcoi  30358  opsqrlem6  30408  stlei  30503  mdslmd1lem1  30588  mdslmd2i  30593  atcvat3i  30659  atcvat4i  30660  sumdmdlem2  30682  dmdbr5ati  30685  xdivpnfrp  31109  oduprs  31144  tpr2rico  31764  ballotlemfp1  32358  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemsup  32371  tgoldbachgt  32543  bnj545  32775  bnj548  32777  satfv1  33225  nosep1o  33811  nodense  33822  bdayimaon  33823  conway  33920  etasslt  33934  slerec  33940  cofcutr  34019  trer  34432  filnetlem3  34496  filnetlem4  34497  phpreu  35688  matunitlindflem1  35700  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem26  35730  mblfinlem1  35741  mblfinlem2  35742  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  prter1  36820  pmapsub  37709  2xp3dxp2ge1d  40090  irrapx1  40566  dfacbasgrp  40849  dgraalem  40886  dgraaub  40889  brcoffn  41529  clsk3nimkb  41539  clsk1indlem1  41544  dvsconst  41837  dvsid  41838  dvsef  41839  islptre  43050  wallispilem1  43496  fourierdlem52  43589  ovnhoilem1  44029  gbowgt5  45102  gboge9  45104  nnsum3primesprm  45130  nnsum3primesgbe  45132  bgoldbnnsum3prm  45144  tgoldbachlt  45156  lincext1  45683  linds0  45694  lindsrng01  45697  lmod1lem3  45718  line2  45986  line2x  45988  inlinecirc02plem  46020  setrec1  46283