Theorem jctil 521

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

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  jctl  525  nic-ax  1676  nic-axALT  1677  unidif  4947  iunxdif2  5057  exss  5464  xpiindi  5836  relssres  6023  frpoinsg  6345  nfunsn  6934  exfo  7107  fliftcnv  7308  oprres  7575  f1oweALT  7959  fo1stres  8001  fo2ndres  8002  dftpos3  8229  wfr3g  8307  tfrlem10  8387  odi  8579  omabs  8650  elixpsn  8931  sbthlem2  9084  sbthlem3  9085  fodomr  9128  mapxpen  9143  pssnn  9168  phplem2OLD  9218  pssnnOLD  9265  oieu  9534  inf3lem6  9628  frmin  9744  frr3g  9751  djuss  9915  acni3  10042  dfacacn  10136  kmlem1  10145  cflm  10245  cfsuc  10252  hsmexlem2  10422  hsmexlem4  10424  hsmexlem5  10425  axdc3lem4  10448  axcclem  10452  brdom5  10524  brdom4  10525  konigthlem  10563  alephval2  10567  alephmul  10573  wunex3  10736  reclem2pr  11043  suplem2pr  11048  lemulge11  12076  nn0ge2m1nn  12541  0mod  13867  1mod  13868  fzennn  13933  hashbclem  14411  hashge2el2dif  14441  wrdlenge2n0  14502  elovmptnn0wrd  14509  swrdnd  14604  s2f1o  14867  f1oun2prg  14868  cotrtrclfv  14959  resqrex  15197  modfsummods  15739  demoivreALT  16144  pcdiv  16785  prmodvdslcmf  16980  invsym2  17710  idghm  19107  gaid  19163  symgsubmefmndALT  19271  subrgid  20321  lbsextlem1  20771  mulgghm2  21046  smadiadet  22172  pmatcollpw3fi  22287  topcld  22539  ntrss  22559  restcld  22676  xkocnv  23318  fbssfi  23341  isfild  23362  alexsublem  23548  alexsubALTlem4  23554  metrest  24033  dscopn  24082  reconnlem1  24342  cphsubrglem  24694  cphipval  24760  itgcnlem  25307  vieta1  25825  jensen  26493  2lgs  26910  nosep1o  27184  nodense  27195  bdayimaon  27196  conway  27300  etasslt  27314  slerec  27320  cofcutr  27411  axlowdimlem6  28205  axlowdimlem7  28206  axlowdimlem16  28215  axlowdimlem17  28216  usgr2v1e2w  28509  0edg0rgr  28829  usgr2wlkspthlem2  29015  clwwlkf1  29302  0pthon  29380  ipval2  29960  sspg  29981  ssps  29983  sspmlem  29985  blocni  30058  ubthlem1  30123  bcsiALT  30432  ocsh  30536  chabs2  30770  pjoml6i  30842  osumcor2i  30897  nmopcoi  31348  opsqrlem6  31398  stlei  31493  mdslmd1lem1  31578  mdslmd2i  31583  atcvat3i  31649  atcvat4i  31650  sumdmdlem2  31672  dmdbr5ati  31675  xdivpnfrp  32099  oduprs  32134  tpr2rico  32892  ballotlemfp1  33490  ballotlemfc0  33491  ballotlemfcc  33492  ballotlemsup  33503  tgoldbachgt  33675  bnj545  33906  bnj548  33908  satfv1  34354  trer  35201  filnetlem3  35265  filnetlem4  35266  phpreu  36472  matunitlindflem1  36484  poimirlem16  36504  poimirlem17  36505  poimirlem19  36507  poimirlem20  36508  poimirlem26  36514  mblfinlem1  36525  mblfinlem2  36526  mblfinlem3  36527  mblfinlem4  36528  ismblfin  36529  prter1  37749  pmapsub  38639  2xp3dxp2ge1d  41022  irrapx1  41566  dfacbasgrp  41850  dgraalem  41887  dgraaub  41890  onexlimgt  41992  cantnftermord  42070  oacl2g  42080  onmcl  42081  omabs2  42082  omcl2  42083  ofoaf  42105  naddwordnexlem3  42150  naddwordnexlem4  42152  brcoffn  42781  clsk3nimkb  42791  clsk1indlem1  42796  dvsconst  43089  dvsid  43090  dvsef  43091  islptre  44335  wallispilem1  44781  fourierdlem52  44874  ovnhoilem1  45317  gbowgt5  46430  gboge9  46432  nnsum3primesprm  46458  nnsum3primesgbe  46460  bgoldbnnsum3prm  46472  tgoldbachlt  46484  lincext1  47135  linds0  47146  lindsrng01  47149  lmod1lem3  47170  line2  47438  line2x  47440  inlinecirc02plem  47472  setrec1  47736