Theorem jctil 522

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  jctl  526  nic-ax  1674  nic-axALT  1675  unidif  4872  iunxdif2  4977  exss  5355  xpiindi  5706  relssres  5893  nfunsn  6707  exfo  6871  fliftcnv  7064  oprres  7316  f1oweALT  7673  fo1stres  7715  fo2ndres  7716  dftpos3  7910  wfr3g  7953  tfrlem10  8023  odi  8205  omabs  8274  elixpsn  8501  sbthlem2  8628  sbthlem3  8629  fodomr  8668  mapxpen  8683  phplem2  8697  pssnn  8736  oieu  9003  inf3lem6  9096  djuss  9349  acni3  9473  dfacacn  9567  kmlem1  9576  cflm  9672  cfsuc  9679  hsmexlem2  9849  hsmexlem4  9851  hsmexlem5  9852  axdc3lem4  9875  axcclem  9879  brdom5  9951  brdom4  9952  konigthlem  9990  alephval2  9994  alephmul  10000  wunex3  10163  reclem2pr  10470  suplem2pr  10475  lemulge11  11502  nn0ge2m1nn  11965  0mod  13271  1mod  13272  fzennn  13337  hashbclem  13811  hashge2el2dif  13839  wrdlenge2n0  13904  elovmptnn0wrd  13911  swrdnd  14016  s2f1o  14278  f1oun2prg  14279  cotrtrclfv  14372  resqrex  14610  modfsummods  15148  demoivreALT  15554  pcdiv  16189  prmodvdslcmf  16383  invsym2  17033  idghm  18373  gaid  18429  symgsubmefmndALT  18531  subrgid  19537  lbsextlem1  19930  mulgghm2  20644  smadiadet  21279  pmatcollpw3fi  21393  topcld  21643  ntrss  21663  restcld  21780  xkocnv  22422  fbssfi  22445  isfild  22466  alexsublem  22652  alexsubALTlem4  22658  metrest  23134  dscopn  23183  reconnlem1  23434  cphsubrglem  23781  cphipval  23846  itgcnlem  24390  vieta1  24901  jensen  25566  2lgs  25983  axlowdimlem6  26733  axlowdimlem7  26734  axlowdimlem16  26743  axlowdimlem17  26744  usgr2v1e2w  27034  0edg0rgr  27354  usgr2wlkspthlem2  27539  clwwlkf1  27828  0pthon  27906  ipval2  28484  sspg  28505  ssps  28507  sspmlem  28509  blocni  28582  ubthlem1  28647  bcsiALT  28956  ocsh  29060  chabs2  29294  pjoml6i  29366  osumcor2i  29421  nmopcoi  29872  opsqrlem6  29922  stlei  30017  mdslmd1lem1  30102  mdslmd2i  30107  atcvat3i  30173  atcvat4i  30174  sumdmdlem2  30196  dmdbr5ati  30199  xdivpnfrp  30609  oduprs  30643  tpr2rico  31155  ballotlemfp1  31749  ballotlemfc0  31750  ballotlemfcc  31751  ballotlemsup  31762  tgoldbachgt  31934  bnj545  32167  bnj548  32169  satfv1  32610  frpoinsg  33081  frr3g  33121  nosep1o  33186  nodense  33196  bdayimaon  33197  nulsslt  33262  conway  33264  etasslt  33274  slerec  33277  trer  33664  filnetlem3  33728  filnetlem4  33729  phpreu  34891  matunitlindflem1  34903  poimirlem16  34923  poimirlem17  34924  poimirlem19  34926  poimirlem20  34927  poimirlem26  34933  mblfinlem1  34944  mblfinlem2  34945  mblfinlem3  34946  mblfinlem4  34947  ismblfin  34948  prter1  36030  pmapsub  36919  2xp3dxp2ge1d  39117  irrapx1  39445  dfacbasgrp  39728  dgraalem  39765  dgraaub  39768  brcoffn  40400  clsk3nimkb  40410  clsk1indlem1  40415  dvsconst  40682  dvsid  40683  dvsef  40684  islptre  41920  wallispilem1  42370  fourierdlem52  42463  ovnhoilem1  42903  gbowgt5  43947  gboge9  43949  nnsum3primesprm  43975  nnsum3primesgbe  43977  bgoldbnnsum3prm  43989  tgoldbachlt  44001  lincext1  44529  linds0  44540  lindsrng01  44543  lmod1lem3  44564  line2  44759  line2x  44761  inlinecirc02plem  44793  setrec1  44814