Theorem jctil 520

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  jctl  524  nic-ax  1675  nic-axALT  1676  unidif  4946  iunxdif2  5056  exss  5463  xpiindi  5835  relssres  6022  frpoinsg  6344  nfunsn  6933  exfo  7106  fliftcnv  7307  oprres  7574  f1oweALT  7958  fo1stres  8000  fo2ndres  8001  dftpos3  8228  wfr3g  8306  tfrlem10  8386  odi  8578  omabs  8649  elixpsn  8930  sbthlem2  9083  sbthlem3  9084  fodomr  9127  mapxpen  9142  pssnn  9167  phplem2OLD  9217  pssnnOLD  9264  oieu  9533  inf3lem6  9627  frmin  9743  frr3g  9750  djuss  9914  acni3  10041  dfacacn  10135  kmlem1  10144  cflm  10244  cfsuc  10251  hsmexlem2  10421  hsmexlem4  10423  hsmexlem5  10424  axdc3lem4  10447  axcclem  10451  brdom5  10523  brdom4  10524  konigthlem  10562  alephval2  10566  alephmul  10572  wunex3  10735  reclem2pr  11042  suplem2pr  11047  lemulge11  12075  nn0ge2m1nn  12540  0mod  13866  1mod  13867  fzennn  13932  hashbclem  14410  hashge2el2dif  14440  wrdlenge2n0  14501  elovmptnn0wrd  14508  swrdnd  14603  s2f1o  14866  f1oun2prg  14867  cotrtrclfv  14958  resqrex  15196  modfsummods  15738  demoivreALT  16143  pcdiv  16784  prmodvdslcmf  16979  invsym2  17709  idghm  19106  gaid  19162  symgsubmefmndALT  19270  subrgid  20320  lbsextlem1  20770  mulgghm2  21045  smadiadet  22171  pmatcollpw3fi  22286  topcld  22538  ntrss  22558  restcld  22675  xkocnv  23317  fbssfi  23340  isfild  23361  alexsublem  23547  alexsubALTlem4  23553  metrest  24032  dscopn  24081  reconnlem1  24341  cphsubrglem  24693  cphipval  24759  itgcnlem  25306  vieta1  25824  jensen  26490  2lgs  26907  nosep1o  27181  nodense  27192  bdayimaon  27193  conway  27297  etasslt  27311  slerec  27317  cofcutr  27408  axlowdimlem6  28202  axlowdimlem7  28203  axlowdimlem16  28212  axlowdimlem17  28213  usgr2v1e2w  28506  0edg0rgr  28826  usgr2wlkspthlem2  29012  clwwlkf1  29299  0pthon  29377  ipval2  29955  sspg  29976  ssps  29978  sspmlem  29980  blocni  30053  ubthlem1  30118  bcsiALT  30427  ocsh  30531  chabs2  30765  pjoml6i  30837  osumcor2i  30892  nmopcoi  31343  opsqrlem6  31393  stlei  31488  mdslmd1lem1  31573  mdslmd2i  31578  atcvat3i  31644  atcvat4i  31645  sumdmdlem2  31667  dmdbr5ati  31670  xdivpnfrp  32094  oduprs  32129  tpr2rico  32887  ballotlemfp1  33485  ballotlemfc0  33486  ballotlemfcc  33487  ballotlemsup  33498  tgoldbachgt  33670  bnj545  33901  bnj548  33903  satfv1  34349  trer  35196  filnetlem3  35260  filnetlem4  35261  phpreu  36467  matunitlindflem1  36479  poimirlem16  36499  poimirlem17  36500  poimirlem19  36502  poimirlem20  36503  poimirlem26  36509  mblfinlem1  36520  mblfinlem2  36521  mblfinlem3  36522  mblfinlem4  36523  ismblfin  36524  prter1  37744  pmapsub  38634  2xp3dxp2ge1d  41017  irrapx1  41556  dfacbasgrp  41840  dgraalem  41877  dgraaub  41880  onexlimgt  41982  cantnftermord  42060  oacl2g  42070  onmcl  42071  omabs2  42072  omcl2  42073  ofoaf  42095  naddwordnexlem3  42140  naddwordnexlem4  42142  brcoffn  42771  clsk3nimkb  42781  clsk1indlem1  42786  dvsconst  43079  dvsid  43080  dvsef  43081  islptre  44325  wallispilem1  44771  fourierdlem52  44864  ovnhoilem1  45307  gbowgt5  46420  gboge9  46422  nnsum3primesprm  46448  nnsum3primesgbe  46450  bgoldbnnsum3prm  46462  tgoldbachlt  46474  lincext1  47125  linds0  47136  lindsrng01  47139  lmod1lem3  47160  line2  47428  line2x  47430  inlinecirc02plem  47462  setrec1  47726