Theorem jctil 518

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

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  jctl  522  nic-ax  1667  nic-axALT  1668  unidif  4946  iunxdif2  5057  exss  5465  xpiindi  5838  relssres  6027  frpoinsg  6351  nfunsn  6938  exfo  7114  fliftcnv  7318  oprres  7589  f1oweALT  7977  fo1stres  8020  fo2ndres  8021  dftpos3  8250  wfr3g  8328  tfrlem10  8408  odi  8600  omabs  8672  elixpsn  8956  sbthlem2  9109  sbthlem3  9110  fodomr  9153  mapxpen  9168  pssnn  9193  phplem2OLD  9243  pssnnOLD  9290  oieu  9564  inf3lem6  9658  frmin  9774  frr3g  9781  djuss  9945  acni3  10072  dfacacn  10166  kmlem1  10175  cflm  10275  cfsuc  10282  hsmexlem2  10452  hsmexlem4  10454  hsmexlem5  10455  axdc3lem4  10478  axcclem  10482  brdom5  10554  brdom4  10555  konigthlem  10593  alephval2  10597  alephmul  10603  wunex3  10766  reclem2pr  11073  suplem2pr  11078  lemulge11  12109  nn0ge2m1nn  12574  0mod  13903  1mod  13904  fzennn  13969  hashbclem  14447  hashge2el2dif  14477  wrdlenge2n0  14538  elovmptnn0wrd  14545  swrdnd  14640  s2f1o  14903  f1oun2prg  14904  cotrtrclfv  14995  resqrex  15233  modfsummods  15775  demoivreALT  16181  pcdiv  16824  prmodvdslcmf  17019  invsym2  17749  idghm  19194  gaid  19262  symgsubmefmndALT  19370  subrgid  20524  lbsextlem1  21058  mulgghm2  21419  smadiadet  22616  pmatcollpw3fi  22731  topcld  22983  ntrss  23003  restcld  23120  xkocnv  23762  fbssfi  23785  isfild  23806  alexsublem  23992  alexsubALTlem4  23998  metrest  24477  dscopn  24526  reconnlem1  24786  cphsubrglem  25149  cphipval  25215  itgcnlem  25763  vieta1  26292  jensen  26966  2lgs  27385  nosep1o  27660  nodense  27671  bdayimaon  27672  conway  27778  etasslt  27792  slerec  27798  cofcutr  27890  om2noseqoi  28226  axlowdimlem6  28830  axlowdimlem7  28831  axlowdimlem16  28840  axlowdimlem17  28841  usgr2v1e2w  29137  0edg0rgr  29458  usgr2wlkspthlem2  29644  clwwlkf1  29931  0pthon  30009  ipval2  30589  sspg  30610  ssps  30612  sspmlem  30614  blocni  30687  ubthlem1  30752  bcsiALT  31061  ocsh  31165  chabs2  31399  pjoml6i  31471  osumcor2i  31526  nmopcoi  31977  opsqrlem6  32027  stlei  32122  mdslmd1lem1  32207  mdslmd2i  32212  atcvat3i  32278  atcvat4i  32279  sumdmdlem2  32301  dmdbr5ati  32304  xdivpnfrp  32741  oduprs  32780  fzo0pmtrlast  32905  tpr2rico  33644  ballotlemfp1  34242  ballotlemfc0  34243  ballotlemfcc  34244  ballotlemsup  34255  tgoldbachgt  34426  bnj545  34657  bnj548  34659  satfv1  35104  trer  35931  filnetlem3  35995  filnetlem4  35996  phpreu  37208  matunitlindflem1  37220  poimirlem16  37240  poimirlem17  37241  poimirlem19  37243  poimirlem20  37244  poimirlem26  37250  mblfinlem1  37261  mblfinlem2  37262  mblfinlem3  37263  mblfinlem4  37264  ismblfin  37265  prter1  38481  pmapsub  39371  2xp3dxp2ge1d  41827  irrapx1  42390  dfacbasgrp  42674  dgraalem  42711  dgraaub  42714  onexlimgt  42813  cantnftermord  42891  oacl2g  42901  onmcl  42902  omabs2  42903  omcl2  42904  ofoaf  42926  naddwordnexlem3  42971  naddwordnexlem4  42973  brcoffn  43602  clsk3nimkb  43612  clsk1indlem1  43617  dvsconst  43909  dvsid  43910  dvsef  43911  islptre  45145  wallispilem1  45591  fourierdlem52  45684  ovnhoilem1  46127  gbowgt5  47239  gboge9  47241  nnsum3primesprm  47267  nnsum3primesgbe  47269  bgoldbnnsum3prm  47281  tgoldbachlt  47293  lincext1  47708  linds0  47719  lindsrng01  47722  lmod1lem3  47743  line2  48011  line2x  48013  inlinecirc02plem  48045  setrec1  48308