Theorem jctil 529

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  jctl  533  nic-ax  1706  nic-axALT  1707  unidif  4908  iunxdif2  5017  exss  5438  xpiindi  5822  relssres  6029  frpoinsg  6372  nfunsn  6955  exfo  7137  fliftcnv  7350  oprres  7620  f1oweALT  8018  fo1stres  8061  fo2ndres  8062  dftpos3  8299  wfr3g  8375  tfrlem10  8433  odi  8625  omabs  8698  elixpsn  9003  sbthlem2  9145  sbthlem3  9146  fodomr  9185  mapxpen  9200  pssnn  9222  oieu  9570  inf3lem6  9671  frmin  9790  frr3g  9797  setrec1  10009  djuss  10038  acni3  10165  dfacacn  10259  kmlem1  10268  cflm  10366  cfsuc  10374  hsmexlem2  10544  hsmexlem4  10546  hsmexlem5  10547  axdc3lem4  10570  axcclem  10574  brdom5  10647  brdom4  10648  konigthlem  10692  alephval2  10696  alephmul  10702  wunex3  10865  reclem2pr  11172  suplem2pr  11177  lemulge11  12219  nn0ge2m1nn  12716  0mod  14082  1mod  14083  fzennn  14151  hashbclem  14638  hashge2el2dif  14666  wrdlenge2n0  14738  elovmptnn0wrd  14745  swrdnd  14846  s2f1o  15110  f1oun2prg  15111  cotrtrclfv  15208  resqrex  15460  modfsummods  16004  demoivreALT  16413  pcdiv  17074  prmodvdslcmf  17269  invsym2  17988  oduprs  18524  chnexg  18842  idghm  19495  gaid  19564  symgsubmefmndALT  19668  subrgid  20876  lbsextlem1  21487  mulgghm2  21837  smadiadet  23040  matunitlindflem1  23049  pmatcollpw3fi  23158  topcld  23408  ntrss  23428  restcld  23545  xkocnv  24188  fbssfi  24211  isfild  24232  alexsublem  24418  alexsubALTlem4  24424  metrest  24898  dscopn  24947  reconnlem1  25201  cphsubrglem  25553  cphipval  25619  itgcnlem  26165  vieta1  26690  jensen  27373  2lgs  27791  fltoprm  28052  nosep1o  28095  nodense  28106  bdayimaon  28107  conway  28222  etaslts  28236  lesrec  28242  cofcutr  28367  om2noseqoi  28746  axlowdimlem6  29582  axlowdimlem7  29583  axlowdimlem16  29592  axlowdimlem17  29593  usgr2v1e2w  29890  0edg0rgr  30210  usgr2wlkspthlem2  30401  clwwlkf1  30697  0pthon  30775  ipval2  31366  sspg  31387  ssps  31389  sspmlem  31391  blocni  31464  ubthlem1  31529  bcsiALT  31838  ocsh  31942  chabs2  32176  pjoml6i  32248  osumcor2i  32303  nmopcoi  32754  opsqrlem6  32804  stlei  32899  mdslmd1lem1  32984  mdslmd2i  32989  atcvat3i  33055  atcvat4i  33056  sumdmdlem2  33078  dmdbr5ati  33081  xdivpnfrp  33595  fzo0pmtrlast  33752  tpr2rico  34655  ballotlemfp1  35235  ballotlemfc0  35236  ballotlemfcc  35237  ballotlemsup  35248  tgoldbachgt  35403  bnj545  35636  bnj548  35638  omeueq  35837  fineqvnttrclse  35933  wevgblacfn  36080  satfv1  36336  trer  37319  filnetlem3  37383  filnetlem4  37384  phpreu  38795  poimirlem16  38822  poimirlem17  38823  poimirlem19  38825  poimirlem20  38826  poimirlem26  38832  mblfinlem1  38843  mblfinlem2  38844  mblfinlem3  38845  mblfinlem4  38846  ismblfin  38847  prter1  40202  pmapsub  41091  irrapx1  44101  dfacbasgrp  44375  dgraalem  44412  dgraaub  44415  onexlimgt  44506  cantnftermord  44583  oacl2g  44593  onmcl  44594  omabs2  44595  omcl2  44596  ofoaf  44618  naddwordnexlem3  44662  naddwordnexlem4  44664  brcoffn  45291  clsk3nimkb  45301  clsk1indlem1  45306  dvsconst  45575  dvsid  45576  dvsef  45577  islptre  46904  wallispilem1  47348  fourierdlem52  47441  ovnhoilem1  47884  sqrtnzqaa  48187  nprmmul3  48884  gbowgt5  49133  gboge9  49135  nnsum3primesprm  49161  nnsum3primesgbe  49163  bgoldbnnsum3prm  49175  tgoldbachlt  49187  stgrnbgr0  49335  grlicref  49383  gpgedg2ov  49437  pgnbgreunbgr  49496  lincext1  49897  linds0  49908  lindsrng01  49911  lmod1lem3  49932  line2  50195  line2x  50197  2oppf  50579