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  4910  iunxdif2  5020  exss  5446  xpiindi  5823  relssres  6023  frpoinsg  6348  nfunsn  6924  exfo  7104  fliftcnv  7315  oprres  7584  f1oweALT  7971  fo1stres  8014  fo2ndres  8015  dftpos3  8242  wfr3g  8318  tfrlem10  8376  odi  8566  omabs  8639  elixpsn  8937  sbthlem2  9079  sbthlem3  9080  fodomr  9119  mapxpen  9134  pssnn  9156  oieu  9504  inf3lem6  9605  frmin  9724  frr3g  9731  djuss  9918  acni3  10043  dfacacn  10137  kmlem1  10146  cflm  10244  cfsuc  10252  hsmexlem2  10422  hsmexlem4  10424  hsmexlem5  10425  axdc3lem4  10448  axcclem  10452  brdom5  10524  brdom4  10525  konigthlem  10564  alephval2  10568  alephmul  10574  wunex3  10737  reclem2pr  11044  suplem2pr  11049  lemulge11  12088  nn0ge2m1nn  12585  0mod  13948  1mod  13949  fzennn  14017  hashbclem  14502  hashge2el2dif  14530  wrdlenge2n0  14602  elovmptnn0wrd  14609  swrdnd  14709  s2f1o  14972  f1oun2prg  14973  cotrtrclfv  15068  resqrex  15320  modfsummods  15863  demoivreALT  16274  pcdiv  16929  prmodvdslcmf  17124  invsym2  17837  oduprs  18373  chnexg  18691  idghm  19324  gaid  19392  symgsubmefmndALT  19496  subrgid  20701  lbsextlem1  21311  mulgghm2  21655  smadiadet  22856  pmatcollpw3fi  22971  topcld  23221  ntrss  23241  restcld  23358  xkocnv  24000  fbssfi  24023  isfild  24044  alexsublem  24230  alexsubALTlem4  24236  metrest  24710  dscopn  24759  reconnlem1  25013  cphsubrglem  25365  cphipval  25431  itgcnlem  25978  vieta1  26502  jensen  27182  2lgs  27600  nosep1o  27874  nodense  27885  bdayimaon  27886  conway  28001  etaslts  28015  lesrec  28021  cofcutr  28146  om2noseqoi  28525  axlowdimlem6  29326  axlowdimlem7  29327  axlowdimlem16  29336  axlowdimlem17  29337  usgr2v1e2w  29631  0edg0rgr  29951  usgr2wlkspthlem2  30136  clwwlkf1  30429  0pthon  30507  ipval2  31088  sspg  31109  ssps  31111  sspmlem  31113  blocni  31186  ubthlem1  31251  bcsiALT  31560  ocsh  31664  chabs2  31898  pjoml6i  31970  osumcor2i  32025  nmopcoi  32476  opsqrlem6  32526  stlei  32621  mdslmd1lem1  32706  mdslmd2i  32711  atcvat3i  32777  atcvat4i  32778  sumdmdlem2  32800  dmdbr5ati  32803  xdivpnfrp  33281  fzo0pmtrlast  33435  tpr2rico  34325  ballotlemfp1  34906  ballotlemfc0  34907  ballotlemfcc  34908  ballotlemsup  34919  tgoldbachgt  35074  bnj545  35307  bnj548  35309  fineqvnttrclse  35553  wevgblacfn  35611  satfv1  35868  trer  36860  filnetlem3  36924  filnetlem4  36925  phpreu  38288  matunitlindflem1  38300  poimirlem16  38320  poimirlem17  38321  poimirlem19  38323  poimirlem20  38324  poimirlem26  38330  mblfinlem1  38341  mblfinlem2  38342  mblfinlem3  38343  mblfinlem4  38344  ismblfin  38345  prter1  39686  pmapsub  40575  irrapx1  43588  dfacbasgrp  43868  dgraalem  43905  dgraaub  43908  onexlimgt  44003  cantnftermord  44080  oacl2g  44090  onmcl  44091  omabs2  44092  omcl2  44093  ofoaf  44115  naddwordnexlem3  44159  naddwordnexlem4  44161  brcoffn  44789  clsk3nimkb  44799  clsk1indlem1  44804  dvsconst  45073  dvsid  45074  dvsef  45075  islptre  46368  wallispilem1  46812  fourierdlem52  46905  ovnhoilem1  47348  sqrtnzqaa  47638  nprmmul3  48311  gbowgt5  48560  gboge9  48562  nnsum3primesprm  48588  nnsum3primesgbe  48590  bgoldbnnsum3prm  48602  tgoldbachlt  48614  stgrnbgr0  48762  grlicref  48810  gpgedg2ov  48864  pgnbgreunbgr  48923  lincext1  49267  linds0  49278  lindsrng01  49281  lmod1lem3  49302  line2  49565  line2x  49567  inlinecirc02plem  49599  2oppf  49943  setrec1  50502