Theorem jctil 523

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

Syntax hints:   → wi 4   ∧ wa 399

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 400

This theorem is referenced by:  jctl  527  nic-ax  1675  nic-axALT  1676  unidif  4834  iunxdif2  4940  exss  5320  xpiindi  5670  relssres  5859  nfunsn  6682  exfo  6848  fliftcnv  7043  oprres  7296  f1oweALT  7655  fo1stres  7697  fo2ndres  7698  dftpos3  7893  wfr3g  7936  tfrlem10  8006  odi  8188  omabs  8257  elixpsn  8484  sbthlem2  8612  sbthlem3  8613  fodomr  8652  mapxpen  8667  phplem2  8681  pssnn  8720  oieu  8987  inf3lem6  9080  djuss  9333  acni3  9458  dfacacn  9552  kmlem1  9561  cflm  9661  cfsuc  9668  hsmexlem2  9838  hsmexlem4  9840  hsmexlem5  9841  axdc3lem4  9864  axcclem  9868  brdom5  9940  brdom4  9941  konigthlem  9979  alephval2  9983  alephmul  9989  wunex3  10152  reclem2pr  10459  suplem2pr  10464  lemulge11  11491  nn0ge2m1nn  11952  0mod  13265  1mod  13266  fzennn  13331  hashbclem  13806  hashge2el2dif  13834  wrdlenge2n0  13895  elovmptnn0wrd  13902  swrdnd  14007  s2f1o  14269  f1oun2prg  14270  cotrtrclfv  14363  resqrex  14602  modfsummods  15140  demoivreALT  15546  pcdiv  16179  prmodvdslcmf  16373  invsym2  17025  idghm  18365  gaid  18421  symgsubmefmndALT  18523  subrgid  19530  lbsextlem1  19923  mulgghm2  20190  smadiadet  21275  pmatcollpw3fi  21390  topcld  21640  ntrss  21660  restcld  21777  xkocnv  22419  fbssfi  22442  isfild  22463  alexsublem  22649  alexsubALTlem4  22655  metrest  23131  dscopn  23180  reconnlem1  23431  cphsubrglem  23782  cphipval  23847  itgcnlem  24393  vieta1  24908  jensen  25574  2lgs  25991  axlowdimlem6  26741  axlowdimlem7  26742  axlowdimlem16  26751  axlowdimlem17  26752  usgr2v1e2w  27042  0edg0rgr  27362  usgr2wlkspthlem2  27547  clwwlkf1  27834  0pthon  27912  ipval2  28490  sspg  28511  ssps  28513  sspmlem  28515  blocni  28588  ubthlem1  28653  bcsiALT  28962  ocsh  29066  chabs2  29300  pjoml6i  29372  osumcor2i  29427  nmopcoi  29878  opsqrlem6  29928  stlei  30023  mdslmd1lem1  30108  mdslmd2i  30113  atcvat3i  30179  atcvat4i  30180  sumdmdlem2  30202  dmdbr5ati  30205  xdivpnfrp  30635  oduprs  30669  tpr2rico  31265  ballotlemfp1  31859  ballotlemfc0  31860  ballotlemfcc  31861  ballotlemsup  31872  tgoldbachgt  32044  bnj545  32277  bnj548  32279  satfv1  32723  frpoinsg  33194  frr3g  33234  nosep1o  33299  nodense  33309  bdayimaon  33310  nulsslt  33375  conway  33377  etasslt  33387  slerec  33390  trer  33777  filnetlem3  33841  filnetlem4  33842  phpreu  35041  matunitlindflem1  35053  poimirlem16  35073  poimirlem17  35074  poimirlem19  35076  poimirlem20  35077  poimirlem26  35083  mblfinlem1  35094  mblfinlem2  35095  mblfinlem3  35096  mblfinlem4  35097  ismblfin  35098  prter1  36175  pmapsub  37064  2xp3dxp2ge1d  39387  irrapx1  39769  dfacbasgrp  40052  dgraalem  40089  dgraaub  40092  brcoffn  40733  clsk3nimkb  40743  clsk1indlem1  40748  dvsconst  41034  dvsid  41035  dvsef  41036  islptre  42261  wallispilem1  42707  fourierdlem52  42800  ovnhoilem1  43240  gbowgt5  44280  gboge9  44282  nnsum3primesprm  44308  nnsum3primesgbe  44310  bgoldbnnsum3prm  44322  tgoldbachlt  44334  lincext1  44863  linds0  44874  lindsrng01  44877  lmod1lem3  44898  line2  45166  line2x  45168  inlinecirc02plem  45200  setrec1  45221