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  1675  nic-axALT  1676  unidif  4900  iunxdif2  5011  exss  5418  xpiindi  5792  relssres  5989  frpoinsg  6309  nfunsn  6881  exfo  7059  fliftcnv  7267  oprres  7536  f1oweALT  7926  fo1stres  7969  fo2ndres  7970  dftpos3  8196  wfr3g  8271  tfrlem10  8328  odi  8516  omabs  8589  elixpsn  8887  sbthlem2  9028  sbthlem3  9029  fodomr  9068  mapxpen  9083  pssnn  9105  oieu  9456  inf3lem6  9554  frmin  9673  frr3g  9680  djuss  9844  acni3  9969  dfacacn  10064  kmlem1  10073  cflm  10172  cfsuc  10179  hsmexlem2  10349  hsmexlem4  10351  hsmexlem5  10352  axdc3lem4  10375  axcclem  10379  brdom5  10451  brdom4  10452  konigthlem  10491  alephval2  10495  alephmul  10501  wunex3  10664  reclem2pr  10971  suplem2pr  10976  lemulge11  12016  nn0ge2m1nn  12483  0mod  13834  1mod  13835  fzennn  13903  hashbclem  14387  hashge2el2dif  14415  wrdlenge2n0  14487  elovmptnn0wrd  14494  swrdnd  14590  s2f1o  14851  f1oun2prg  14852  cotrtrclfv  14947  resqrex  15185  modfsummods  15728  demoivreALT  16138  pcdiv  16792  prmodvdslcmf  16987  invsym2  17699  oduprs  18235  chnexg  18553  idghm  19172  gaid  19240  symgsubmefmndALT  19344  subrgid  20518  lbsextlem1  21125  mulgghm2  21443  smadiadet  22626  pmatcollpw3fi  22741  topcld  22991  ntrss  23011  restcld  23128  xkocnv  23770  fbssfi  23793  isfild  23814  alexsublem  24000  alexsubALTlem4  24006  metrest  24480  dscopn  24529  reconnlem1  24783  cphsubrglem  25145  cphipval  25211  itgcnlem  25759  vieta1  26288  jensen  26967  2lgs  27386  nosep1o  27661  nodense  27672  bdayimaon  27673  conway  27787  etaslts  27801  lesrec  27807  cofcutr  27932  om2noseqoi  28311  axlowdimlem6  29032  axlowdimlem7  29033  axlowdimlem16  29042  axlowdimlem17  29043  usgr2v1e2w  29337  0edg0rgr  29658  usgr2wlkspthlem2  29843  clwwlkf1  30136  0pthon  30214  ipval2  30794  sspg  30815  ssps  30817  sspmlem  30819  blocni  30892  ubthlem1  30957  bcsiALT  31266  ocsh  31370  chabs2  31604  pjoml6i  31676  osumcor2i  31731  nmopcoi  32182  opsqrlem6  32232  stlei  32327  mdslmd1lem1  32412  mdslmd2i  32417  atcvat3i  32483  atcvat4i  32484  sumdmdlem2  32506  dmdbr5ati  32509  xdivpnfrp  33024  fzo0pmtrlast  33185  tpr2rico  34089  ballotlemfp1  34669  ballotlemfc0  34670  ballotlemfcc  34671  ballotlemsup  34682  tgoldbachgt  34840  bnj545  35070  bnj548  35072  fineqvnttrclse  35299  wevgblacfn  35322  satfv1  35576  trer  36529  filnetlem3  36593  filnetlem4  36594  phpreu  37852  matunitlindflem1  37864  poimirlem16  37884  poimirlem17  37885  poimirlem19  37887  poimirlem20  37888  poimirlem26  37894  mblfinlem1  37905  mblfinlem2  37906  mblfinlem3  37907  mblfinlem4  37908  ismblfin  37909  prter1  39252  pmapsub  40141  irrapx1  43182  dfacbasgrp  43462  dgraalem  43499  dgraaub  43502  onexlimgt  43597  cantnftermord  43674  oacl2g  43684  onmcl  43685  omabs2  43686  omcl2  43687  ofoaf  43709  naddwordnexlem3  43753  naddwordnexlem4  43755  brcoffn  44383  clsk3nimkb  44393  clsk1indlem1  44398  dvsconst  44683  dvsid  44684  dvsef  44685  islptre  45976  wallispilem1  46420  fourierdlem52  46513  ovnhoilem1  46956  gbowgt5  48119  gboge9  48121  nnsum3primesprm  48147  nnsum3primesgbe  48149  bgoldbnnsum3prm  48161  tgoldbachlt  48173  stgrnbgr0  48321  grlicref  48369  gpgedg2ov  48423  pgnbgreunbgr  48482  lincext1  48811  linds0  48822  lindsrng01  48825  lmod1lem3  48846  line2  49109  line2x  49111  inlinecirc02plem  49143  2oppf  49488  setrec1  50047