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  1672  nic-axALT  1673  unidif  4916  iunxdif2  5027  exss  5436  xpiindi  5813  relssres  6007  frpoinsg  6330  nfunsn  6915  exfo  7092  fliftcnv  7300  oprres  7570  f1oweALT  7966  fo1stres  8009  fo2ndres  8010  dftpos3  8238  wfr3g  8316  tfrlem10  8396  odi  8586  omabs  8658  elixpsn  8946  sbthlem2  9093  sbthlem3  9094  fodomr  9137  mapxpen  9152  pssnn  9177  phplem2OLD  9224  oieu  9546  inf3lem6  9640  frmin  9756  frr3g  9763  djuss  9927  acni3  10054  dfacacn  10149  kmlem1  10158  cflm  10257  cfsuc  10264  hsmexlem2  10434  hsmexlem4  10436  hsmexlem5  10437  axdc3lem4  10460  axcclem  10464  brdom5  10536  brdom4  10537  konigthlem  10575  alephval2  10579  alephmul  10585  wunex3  10748  reclem2pr  11055  suplem2pr  11060  lemulge11  12097  nn0ge2m1nn  12564  0mod  13909  1mod  13910  fzennn  13976  hashbclem  14460  hashge2el2dif  14488  wrdlenge2n0  14559  elovmptnn0wrd  14566  swrdnd  14661  s2f1o  14924  f1oun2prg  14925  cotrtrclfv  15020  resqrex  15258  modfsummods  15798  demoivreALT  16206  pcdiv  16859  prmodvdslcmf  17054  invsym2  17763  oduprs  18299  idghm  19201  gaid  19269  symgsubmefmndALT  19371  subrgid  20520  lbsextlem1  21106  mulgghm2  21424  smadiadet  22595  pmatcollpw3fi  22710  topcld  22960  ntrss  22980  restcld  23097  xkocnv  23739  fbssfi  23762  isfild  23783  alexsublem  23969  alexsubALTlem4  23975  metrest  24450  dscopn  24499  reconnlem1  24753  cphsubrglem  25116  cphipval  25182  itgcnlem  25730  vieta1  26259  jensen  26937  2lgs  27356  nosep1o  27631  nodense  27642  bdayimaon  27643  conway  27749  etasslt  27763  slerec  27769  cofcutr  27863  om2noseqoi  28214  axlowdimlem6  28860  axlowdimlem7  28861  axlowdimlem16  28870  axlowdimlem17  28871  usgr2v1e2w  29165  0edg0rgr  29486  usgr2wlkspthlem2  29674  clwwlkf1  29964  0pthon  30042  ipval2  30622  sspg  30643  ssps  30645  sspmlem  30647  blocni  30720  ubthlem1  30785  bcsiALT  31094  ocsh  31198  chabs2  31432  pjoml6i  31504  osumcor2i  31559  nmopcoi  32010  opsqrlem6  32060  stlei  32155  mdslmd1lem1  32240  mdslmd2i  32245  atcvat3i  32311  atcvat4i  32312  sumdmdlem2  32334  dmdbr5ati  32337  xdivpnfrp  32844  fzo0pmtrlast  33040  tpr2rico  33872  ballotlemfp1  34453  ballotlemfc0  34454  ballotlemfcc  34455  ballotlemsup  34466  tgoldbachgt  34624  bnj545  34855  bnj548  34857  wevgblacfn  35060  satfv1  35314  trer  36263  filnetlem3  36327  filnetlem4  36328  phpreu  37557  matunitlindflem1  37569  poimirlem16  37589  poimirlem17  37590  poimirlem19  37592  poimirlem20  37593  poimirlem26  37599  mblfinlem1  37610  mblfinlem2  37611  mblfinlem3  37612  mblfinlem4  37613  ismblfin  37614  prter1  38826  pmapsub  39716  2xp3dxp2ge1d  42183  irrapx1  42783  dfacbasgrp  43064  dgraalem  43101  dgraaub  43104  onexlimgt  43199  cantnftermord  43276  oacl2g  43286  onmcl  43287  omabs2  43288  omcl2  43289  ofoaf  43311  naddwordnexlem3  43355  naddwordnexlem4  43357  brcoffn  43986  clsk3nimkb  43996  clsk1indlem1  44001  dvsconst  44287  dvsid  44288  dvsef  44289  islptre  45584  wallispilem1  46030  fourierdlem52  46123  ovnhoilem1  46566  gbowgt5  47702  gboge9  47704  nnsum3primesprm  47730  nnsum3primesgbe  47732  bgoldbnnsum3prm  47744  tgoldbachlt  47756  stgrnbgr0  47884  grlicref  47925  lincext1  48324  linds0  48335  lindsrng01  48338  lmod1lem3  48359  line2  48626  line2x  48628  inlinecirc02plem  48660  setrec1  49396