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  1703  nic-axALT  1704  unidif  4909  iunxdif2  5019  exss  5446  xpiindi  5823  relssres  6023  frpoinsg  6346  nfunsn  6922  exfo  7102  fliftcnv  7311  oprres  7580  f1oweALT  7970  fo1stres  8013  fo2ndres  8014  dftpos3  8241  wfr3g  8317  tfrlem10  8375  odi  8565  omabs  8638  elixpsn  8936  sbthlem2  9077  sbthlem3  9078  fodomr  9117  mapxpen  9132  pssnn  9154  oieu  9502  inf3lem6  9603  frmin  9722  frr3g  9729  djuss  9907  acni3  10032  dfacacn  10126  kmlem1  10135  cflm  10234  cfsuc  10242  hsmexlem2  10412  hsmexlem4  10414  hsmexlem5  10415  axdc3lem4  10438  axcclem  10442  brdom5  10514  brdom4  10515  konigthlem  10554  alephval2  10558  alephmul  10564  wunex3  10727  reclem2pr  11034  suplem2pr  11039  lemulge11  12078  nn0ge2m1nn  12575  0mod  13937  1mod  13938  fzennn  14006  hashbclem  14491  hashge2el2dif  14519  wrdlenge2n0  14591  elovmptnn0wrd  14598  swrdnd  14694  s2f1o  14955  f1oun2prg  14956  cotrtrclfv  15051  resqrex  15303  modfsummods  15847  demoivreALT  16258  pcdiv  16913  prmodvdslcmf  17108  invsym2  17821  oduprs  18357  chnexg  18675  idghm  19302  gaid  19370  symgsubmefmndALT  19474  subrgid  20659  lbsextlem1  21263  mulgghm2  21607  smadiadet  22808  pmatcollpw3fi  22923  topcld  23173  ntrss  23193  restcld  23310  xkocnv  23952  fbssfi  23975  isfild  23996  alexsublem  24182  alexsubALTlem4  24188  metrest  24662  dscopn  24711  reconnlem1  24965  cphsubrglem  25317  cphipval  25383  itgcnlem  25930  vieta1  26454  jensen  27134  2lgs  27552  nosep1o  27826  nodense  27837  bdayimaon  27838  conway  27953  etaslts  27967  lesrec  27973  cofcutr  28098  om2noseqoi  28477  axlowdimlem6  29278  axlowdimlem7  29279  axlowdimlem16  29288  axlowdimlem17  29289  usgr2v1e2w  29583  0edg0rgr  29903  usgr2wlkspthlem2  30088  clwwlkf1  30381  0pthon  30459  ipval2  31040  sspg  31061  ssps  31063  sspmlem  31065  blocni  31138  ubthlem1  31203  bcsiALT  31512  ocsh  31616  chabs2  31850  pjoml6i  31922  osumcor2i  31977  nmopcoi  32428  opsqrlem6  32478  stlei  32573  mdslmd1lem1  32658  mdslmd2i  32663  atcvat3i  32729  atcvat4i  32730  sumdmdlem2  32752  dmdbr5ati  32755  xdivpnfrp  33233  fzo0pmtrlast  33393  tpr2rico  34283  ballotlemfp1  34863  ballotlemfc0  34864  ballotlemfcc  34865  ballotlemsup  34876  tgoldbachgt  35031  bnj545  35264  bnj548  35266  fineqvnttrclse  35518  wevgblacfn  35576  satfv1  35836  trer  36808  filnetlem3  36872  filnetlem4  36873  phpreu  38236  matunitlindflem1  38248  poimirlem16  38268  poimirlem17  38269  poimirlem19  38271  poimirlem20  38272  poimirlem26  38278  mblfinlem1  38289  mblfinlem2  38290  mblfinlem3  38291  mblfinlem4  38292  ismblfin  38293  prter1  39634  pmapsub  40523  irrapx1  43538  dfacbasgrp  43818  dgraalem  43855  dgraaub  43858  onexlimgt  43953  cantnftermord  44030  oacl2g  44040  onmcl  44041  omabs2  44042  omcl2  44043  ofoaf  44065  naddwordnexlem3  44109  naddwordnexlem4  44111  brcoffn  44739  clsk3nimkb  44749  clsk1indlem1  44754  dvsconst  45023  dvsid  45024  dvsef  45025  islptre  46318  wallispilem1  46762  fourierdlem52  46855  ovnhoilem1  47298  sqrtnzqaa  47588  nprmmul3  48261  gbowgt5  48510  gboge9  48512  nnsum3primesprm  48538  nnsum3primesgbe  48540  bgoldbnnsum3prm  48552  tgoldbachlt  48564  stgrnbgr0  48712  grlicref  48760  gpgedg2ov  48814  pgnbgreunbgr  48873  lincext1  49217  linds0  49228  lindsrng01  49231  lmod1lem3  49252  line2  49515  line2x  49517  inlinecirc02plem  49549  2oppf  49893  setrec1  50452