Theorem jctil 528

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  jctl  532  nic-ax  1696  nic-axALT  1697  unidif  4903  iunxdif2  5013  exss  5434  xpiindi  5811  relssres  6011  frpoinsg  6333  nfunsn  6910  exfo  7090  fliftcnv  7299  oprres  7568  f1oweALT  7957  fo1stres  8000  fo2ndres  8001  dftpos3  8228  wfr3g  8304  tfrlem10  8362  odi  8552  omabs  8625  elixpsn  8923  sbthlem2  9064  sbthlem3  9065  fodomr  9104  mapxpen  9119  pssnn  9141  oieu  9489  inf3lem6  9590  frmin  9709  frr3g  9716  djuss  9894  acni3  10019  dfacacn  10113  kmlem1  10122  cflm  10221  cfsuc  10229  hsmexlem2  10399  hsmexlem4  10401  hsmexlem5  10402  axdc3lem4  10425  axcclem  10429  brdom5  10501  brdom4  10502  konigthlem  10541  alephval2  10545  alephmul  10551  wunex3  10714  reclem2pr  11021  suplem2pr  11026  lemulge11  12065  nn0ge2m1nn  12562  0mod  13923  1mod  13924  fzennn  13992  hashbclem  14477  hashge2el2dif  14505  wrdlenge2n0  14577  elovmptnn0wrd  14584  swrdnd  14680  s2f1o  14941  f1oun2prg  14942  cotrtrclfv  15037  resqrex  15289  modfsummods  15833  demoivreALT  16245  pcdiv  16900  prmodvdslcmf  17095  invsym2  17808  oduprs  18344  chnexg  18662  idghm  19289  gaid  19357  symgsubmefmndALT  19461  subrgid  20646  lbsextlem1  21248  mulgghm2  21583  smadiadet  22784  pmatcollpw3fi  22899  topcld  23149  ntrss  23169  restcld  23286  xkocnv  23928  fbssfi  23951  isfild  23972  alexsublem  24158  alexsubALTlem4  24164  metrest  24638  dscopn  24687  reconnlem1  24941  cphsubrglem  25293  cphipval  25359  itgcnlem  25906  vieta1  26430  jensen  27107  2lgs  27525  nosep1o  27799  nodense  27810  bdayimaon  27811  conway  27926  etaslts  27940  lesrec  27946  cofcutr  28071  om2noseqoi  28450  axlowdimlem6  29202  axlowdimlem7  29203  axlowdimlem16  29212  axlowdimlem17  29213  usgr2v1e2w  29507  0edg0rgr  29827  usgr2wlkspthlem2  30012  clwwlkf1  30305  0pthon  30383  ipval2  30964  sspg  30985  ssps  30987  sspmlem  30989  blocni  31062  ubthlem1  31127  bcsiALT  31436  ocsh  31540  chabs2  31774  pjoml6i  31846  osumcor2i  31901  nmopcoi  32352  opsqrlem6  32402  stlei  32497  mdslmd1lem1  32582  mdslmd2i  32587  atcvat3i  32653  atcvat4i  32654  sumdmdlem2  32676  dmdbr5ati  32679  xdivpnfrp  33160  fzo0pmtrlast  33320  tpr2rico  34214  ballotlemfp1  34794  ballotlemfc0  34795  ballotlemfcc  34796  ballotlemsup  34807  tgoldbachgt  34962  bnj545  35195  bnj548  35197  fineqvnttrclse  35427  wevgblacfn  35461  satfv1  35721  trer  36684  filnetlem3  36748  filnetlem4  36749  phpreu  38110  matunitlindflem1  38122  poimirlem16  38142  poimirlem17  38143  poimirlem19  38145  poimirlem20  38146  poimirlem26  38152  mblfinlem1  38163  mblfinlem2  38164  mblfinlem3  38165  mblfinlem4  38166  ismblfin  38167  prter1  39510  pmapsub  40399  irrapx1  43412  dfacbasgrp  43692  dgraalem  43729  dgraaub  43732  onexlimgt  43827  cantnftermord  43904  oacl2g  43914  onmcl  43915  omabs2  43916  omcl2  43917  ofoaf  43939  naddwordnexlem3  43983  naddwordnexlem4  43985  brcoffn  44613  clsk3nimkb  44623  clsk1indlem1  44628  dvsconst  44899  dvsid  44900  dvsef  44901  islptre  46194  wallispilem1  46638  fourierdlem52  46731  ovnhoilem1  47174  nprmmul3  48134  gbowgt5  48383  gboge9  48385  nnsum3primesprm  48411  nnsum3primesgbe  48413  bgoldbnnsum3prm  48425  tgoldbachlt  48437  stgrnbgr0  48585  grlicref  48633  gpgedg2ov  48687  pgnbgreunbgr  48746  lincext1  49086  linds0  49097  lindsrng01  49100  lmod1lem3  49121  line2  49384  line2x  49386  inlinecirc02plem  49418  2oppf  49762  setrec1  50321