Theorem jctil 529

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  jctl  533  nic-ax  1706  nic-axALT  1707  unidif  4903  iunxdif2  5012  exss  5438  xpiindi  5815  relssres  6015  frpoinsg  6341  nfunsn  6917  exfo  7098  fliftcnv  7312  oprres  7581  f1oweALT  7969  fo1stres  8012  fo2ndres  8013  dftpos3  8242  wfr3g  8318  tfrlem10  8376  odi  8566  omabs  8639  elixpsn  8944  sbthlem2  9086  sbthlem3  9087  fodomr  9126  mapxpen  9141  pssnn  9163  oieu  9511  inf3lem6  9612  frmin  9731  frr3g  9738  djuss  9925  acni3  10050  dfacacn  10144  kmlem1  10153  cflm  10251  cfsuc  10259  hsmexlem2  10429  hsmexlem4  10431  hsmexlem5  10432  axdc3lem4  10455  axcclem  10459  brdom5  10532  brdom4  10533  konigthlem  10577  alephval2  10581  alephmul  10587  wunex3  10750  reclem2pr  11057  suplem2pr  11062  lemulge11  12101  nn0ge2m1nn  12598  0mod  13963  1mod  13964  fzennn  14032  hashbclem  14517  hashge2el2dif  14545  wrdlenge2n0  14617  elovmptnn0wrd  14624  swrdnd  14724  s2f1o  14987  f1oun2prg  14988  cotrtrclfv  15085  resqrex  15337  modfsummods  15880  demoivreALT  16289  pcdiv  16944  prmodvdslcmf  17139  invsym2  17852  oduprs  18388  chnexg  18706  idghm  19358  gaid  19426  symgsubmefmndALT  19530  subrgid  20735  lbsextlem1  21345  mulgghm2  21689  smadiadet  22892  matunitlindflem1  22901  pmatcollpw3fi  23010  topcld  23260  ntrss  23280  restcld  23397  xkocnv  24040  fbssfi  24063  isfild  24084  alexsublem  24270  alexsubALTlem4  24276  metrest  24750  dscopn  24799  reconnlem1  25053  cphsubrglem  25405  cphipval  25471  itgcnlem  26017  vieta1  26544  jensen  27225  2lgs  27643  nosep1o  27917  nodense  27928  bdayimaon  27929  conway  28044  etaslts  28058  lesrec  28064  cofcutr  28189  om2noseqoi  28568  axlowdimlem6  29404  axlowdimlem7  29405  axlowdimlem16  29414  axlowdimlem17  29415  usgr2v1e2w  29712  0edg0rgr  30032  usgr2wlkspthlem2  30223  clwwlkf1  30519  0pthon  30597  ipval2  31188  sspg  31209  ssps  31211  sspmlem  31213  blocni  31286  ubthlem1  31351  bcsiALT  31660  ocsh  31764  chabs2  31998  pjoml6i  32070  osumcor2i  32125  nmopcoi  32576  opsqrlem6  32626  stlei  32721  mdslmd1lem1  32806  mdslmd2i  32811  atcvat3i  32877  atcvat4i  32878  sumdmdlem2  32900  dmdbr5ati  32903  xdivpnfrp  33378  fzo0pmtrlast  33532  tpr2rico  34422  ballotlemfp1  35003  ballotlemfc0  35004  ballotlemfcc  35005  ballotlemsup  35016  tgoldbachgt  35171  bnj545  35404  bnj548  35406  fineqvnttrclse  35650  wevgblacfn  35708  satfv1  35942  trer  36935  filnetlem3  36999  filnetlem4  37000  phpreu  38358  poimirlem16  38385  poimirlem17  38386  poimirlem19  38388  poimirlem20  38389  poimirlem26  38395  mblfinlem1  38406  mblfinlem2  38407  mblfinlem3  38408  mblfinlem4  38409  ismblfin  38410  prter1  39752  pmapsub  40641  irrapx1  43669  dfacbasgrp  43949  dgraalem  43986  dgraaub  43989  onexlimgt  44084  cantnftermord  44161  oacl2g  44171  onmcl  44172  omabs2  44173  omcl2  44174  ofoaf  44196  naddwordnexlem3  44240  naddwordnexlem4  44242  brcoffn  44870  clsk3nimkb  44880  clsk1indlem1  44885  dvsconst  45154  dvsid  45155  dvsef  45156  islptre  46449  wallispilem1  46893  fourierdlem52  46986  ovnhoilem1  47429  sqrtnzqaa  47732  nprmmul3  48429  gbowgt5  48678  gboge9  48680  nnsum3primesprm  48706  nnsum3primesgbe  48708  bgoldbnnsum3prm  48720  tgoldbachlt  48732  stgrnbgr0  48880  grlicref  48928  gpgedg2ov  48982  pgnbgreunbgr  49041  lincext1  49384  linds0  49395  lindsrng01  49398  lmod1lem3  49419  line2  49682  line2x  49684  inlinecirc02plem  49716  2oppf  50058  setrec1  50617