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  5431  xpiindi  5812  relssres  6011  frpoinsg  6345  nfunsn  6922  exfo  7103  fliftcnv  7317  oprres  7586  f1oweALT  7982  fo1stres  8025  fo2ndres  8026  dftpos3  8254  wfr3g  8330  tfrlem10  8388  odi  8580  omabs  8653  elixpsn  8958  sbthlem2  9100  sbthlem3  9101  fodomr  9140  mapxpen  9155  pssnn  9177  oieu  9526  inf3lem6  9627  frmin  9746  frr3g  9753  setrec1  9965  djuss  9994  acni3  10119  dfacacn  10213  kmlem1  10222  cflm  10320  cfsuc  10328  hsmexlem2  10498  hsmexlem4  10500  hsmexlem5  10501  axdc3lem4  10524  axcclem  10528  brdom5  10601  brdom4  10602  konigthlem  10646  alephval2  10650  alephmul  10656  wunex3  10819  reclem2pr  11126  suplem2pr  11131  lemulge11  12172  nn0ge2m1nn  12669  0mod  14035  1mod  14036  fzennn  14104  hashbclem  14590  hashge2el2dif  14618  wrdlenge2n0  14690  elovmptnn0wrd  14697  swrdnd  14797  s2f1o  15060  f1oun2prg  15061  cotrtrclfv  15158  resqrex  15410  modfsummods  15953  demoivreALT  16362  pcdiv  17023  prmodvdslcmf  17218  invsym2  17931  oduprs  18467  chnexg  18785  idghm  19438  gaid  19506  symgsubmefmndALT  19610  subrgid  20818  lbsextlem1  21429  mulgghm2  21775  smadiadet  22978  matunitlindflem1  22987  pmatcollpw3fi  23096  topcld  23346  ntrss  23366  restcld  23483  xkocnv  24126  fbssfi  24149  isfild  24170  alexsublem  24356  alexsubALTlem4  24362  metrest  24836  dscopn  24885  reconnlem1  25139  cphsubrglem  25491  cphipval  25557  itgcnlem  26103  vieta1  26628  jensen  27309  2lgs  27727  fltoprm  27988  nosep1o  28031  nodense  28042  bdayimaon  28043  conway  28158  etaslts  28172  lesrec  28178  cofcutr  28303  om2noseqoi  28682  axlowdimlem6  29518  axlowdimlem7  29519  axlowdimlem16  29528  axlowdimlem17  29529  usgr2v1e2w  29826  0edg0rgr  30146  usgr2wlkspthlem2  30337  clwwlkf1  30633  0pthon  30711  ipval2  31302  sspg  31323  ssps  31325  sspmlem  31327  blocni  31400  ubthlem1  31465  bcsiALT  31774  ocsh  31878  chabs2  32112  pjoml6i  32184  osumcor2i  32239  nmopcoi  32690  opsqrlem6  32740  stlei  32835  mdslmd1lem1  32920  mdslmd2i  32925  atcvat3i  32991  atcvat4i  32992  sumdmdlem2  33014  dmdbr5ati  33017  xdivpnfrp  33492  fzo0pmtrlast  33646  tpr2rico  34537  ballotlemfp1  35117  ballotlemfc0  35118  ballotlemfcc  35119  ballotlemsup  35130  tgoldbachgt  35285  bnj545  35518  bnj548  35520  fineqvnttrclse  35775  wevgblacfn  35873  satfv1  36107  trer  37084  filnetlem3  37148  filnetlem4  37149  phpreu  38507  poimirlem16  38534  poimirlem17  38535  poimirlem19  38537  poimirlem20  38538  poimirlem26  38544  mblfinlem1  38555  mblfinlem2  38556  mblfinlem3  38557  mblfinlem4  38558  ismblfin  38559  prter1  39916  pmapsub  40805  irrapx1  43814  dfacbasgrp  44094  dgraalem  44131  dgraaub  44134  onexlimgt  44229  cantnftermord  44306  oacl2g  44316  onmcl  44317  omabs2  44318  omcl2  44319  ofoaf  44341  naddwordnexlem3  44385  naddwordnexlem4  44387  brcoffn  45015  clsk3nimkb  45025  clsk1indlem1  45030  dvsconst  45299  dvsid  45300  dvsef  45301  islptre  46600  wallispilem1  47044  fourierdlem52  47137  ovnhoilem1  47580  sqrtnzqaa  47883  nprmmul3  48580  gbowgt5  48829  gboge9  48831  nnsum3primesprm  48857  nnsum3primesgbe  48859  bgoldbnnsum3prm  48871  tgoldbachlt  48883  stgrnbgr0  49031  grlicref  49079  gpgedg2ov  49133  pgnbgreunbgr  49192  lincext1  49535  linds0  49546  lindsrng01  49549  lmod1lem3  49570  line2  49833  line2x  49835  inlinecirc02plem  49867  2oppf  50209