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  1705  nic-axALT  1706  unidif  4902  iunxdif2  5011  exss  5430  xpiindi  5811  relssres  6010  frpoinsg  6346  nfunsn  6925  exfo  7106  fliftcnv  7320  oprres  7589  f1oweALT  7985  fo1stres  8028  fo2ndres  8029  dftpos3  8265  wfr3g  8341  tfrlem10  8399  odi  8591  omabs  8664  elixpsn  8969  sbthlem2  9111  sbthlem3  9112  fodomr  9151  mapxpen  9166  pssnn  9188  oieu  9537  inf3lem6  9638  frmin  9757  frr3g  9764  setrec1  9976  djuss  10005  acni3  10130  dfacacn  10224  kmlem1  10233  cflm  10331  cfsuc  10339  hsmexlem2  10509  hsmexlem4  10511  hsmexlem5  10512  axdc3lem4  10535  axcclem  10539  brdom5  10612  brdom4  10613  konigthlem  10657  alephval2  10661  alephmul  10667  wunex3  10830  reclem2pr  11137  suplem2pr  11142  lemulge11  12183  nn0ge2m1nn  12680  0mod  14046  1mod  14047  fzennn  14115  hashbclem  14601  hashge2el2dif  14629  wrdlenge2n0  14701  elovmptnn0wrd  14708  swrdnd  14809  s2f1o  15073  f1oun2prg  15074  cotrtrclfv  15171  resqrex  15423  modfsummods  15966  demoivreALT  16375  pcdiv  17036  prmodvdslcmf  17231  invsym2  17944  oduprs  18480  chnexg  18798  idghm  19451  gaid  19519  symgsubmefmndALT  19623  subrgid  20831  lbsextlem1  21442  mulgghm2  21788  smadiadet  22991  matunitlindflem1  23000  pmatcollpw3fi  23109  topcld  23359  ntrss  23379  restcld  23496  xkocnv  24139  fbssfi  24162  isfild  24183  alexsublem  24369  alexsubALTlem4  24375  metrest  24849  dscopn  24898  reconnlem1  25152  cphsubrglem  25504  cphipval  25570  itgcnlem  26116  vieta1  26641  jensen  27322  2lgs  27740  fltoprm  28001  nosep1o  28044  nodense  28055  bdayimaon  28056  conway  28171  etaslts  28185  lesrec  28191  cofcutr  28316  om2noseqoi  28695  axlowdimlem6  29531  axlowdimlem7  29532  axlowdimlem16  29541  axlowdimlem17  29542  usgr2v1e2w  29839  0edg0rgr  30159  usgr2wlkspthlem2  30350  clwwlkf1  30646  0pthon  30724  ipval2  31315  sspg  31336  ssps  31338  sspmlem  31340  blocni  31413  ubthlem1  31478  bcsiALT  31787  ocsh  31891  chabs2  32125  pjoml6i  32197  osumcor2i  32252  nmopcoi  32703  opsqrlem6  32753  stlei  32848  mdslmd1lem1  32933  mdslmd2i  32938  atcvat3i  33004  atcvat4i  33005  sumdmdlem2  33027  dmdbr5ati  33030  xdivpnfrp  33546  fzo0pmtrlast  33700  tpr2rico  34591  ballotlemfp1  35171  ballotlemfc0  35172  ballotlemfcc  35173  ballotlemsup  35184  tgoldbachgt  35339  bnj545  35572  bnj548  35574  fineqvnttrclse  35849  wevgblacfn  35959  satfv1  36215  trer  37197  filnetlem3  37261  filnetlem4  37262  phpreu  38621  poimirlem16  38648  poimirlem17  38649  poimirlem19  38651  poimirlem20  38652  poimirlem26  38658  mblfinlem1  38669  mblfinlem2  38670  mblfinlem3  38671  mblfinlem4  38672  ismblfin  38673  prter1  40030  pmapsub  40919  irrapx1  43929  dfacbasgrp  44204  dgraalem  44241  dgraaub  44244  onexlimgt  44339  cantnftermord  44416  oacl2g  44426  onmcl  44427  omabs2  44428  omcl2  44429  ofoaf  44451  naddwordnexlem3  44495  naddwordnexlem4  44497  brcoffn  45124  clsk3nimkb  45134  clsk1indlem1  45139  dvsconst  45408  dvsid  45409  dvsef  45410  islptre  46725  wallispilem1  47169  fourierdlem52  47262  ovnhoilem1  47705  sqrtnzqaa  48008  nprmmul3  48705  gbowgt5  48954  gboge9  48956  nnsum3primesprm  48982  nnsum3primesgbe  48984  bgoldbnnsum3prm  48996  tgoldbachlt  49008  stgrnbgr0  49156  grlicref  49204  gpgedg2ov  49258  pgnbgreunbgr  49317  lincext1  49660  linds0  49671  lindsrng01  49674  lmod1lem3  49695  line2  49958  line2x  49960  2oppf  50342