Theorem jctil 519

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  jctl  523  nic-ax  1673  nic-axALT  1674  unidif  4923  iunxdif2  5034  exss  5443  xpiindi  5820  relssres  6014  frpoinsg  6337  nfunsn  6923  exfo  7100  fliftcnv  7309  oprres  7580  f1oweALT  7976  fo1stres  8019  fo2ndres  8020  dftpos3  8248  wfr3g  8326  tfrlem10  8406  odi  8596  omabs  8668  elixpsn  8956  sbthlem2  9103  sbthlem3  9104  fodomr  9147  mapxpen  9162  pssnn  9187  phplem2OLD  9234  oieu  9558  inf3lem6  9652  frmin  9768  frr3g  9775  djuss  9939  acni3  10066  dfacacn  10161  kmlem1  10170  cflm  10269  cfsuc  10276  hsmexlem2  10446  hsmexlem4  10448  hsmexlem5  10449  axdc3lem4  10472  axcclem  10476  brdom5  10548  brdom4  10549  konigthlem  10587  alephval2  10591  alephmul  10597  wunex3  10760  reclem2pr  11067  suplem2pr  11072  lemulge11  12109  nn0ge2m1nn  12576  0mod  13924  1mod  13925  fzennn  13991  hashbclem  14475  hashge2el2dif  14503  wrdlenge2n0  14575  elovmptnn0wrd  14582  swrdnd  14677  s2f1o  14940  f1oun2prg  14941  cotrtrclfv  15036  resqrex  15274  modfsummods  15814  demoivreALT  16224  pcdiv  16877  prmodvdslcmf  17072  invsym2  17781  oduprs  18317  idghm  19219  gaid  19287  symgsubmefmndALT  19389  subrgid  20538  lbsextlem1  21124  mulgghm2  21442  smadiadet  22613  pmatcollpw3fi  22728  topcld  22978  ntrss  22998  restcld  23115  xkocnv  23757  fbssfi  23780  isfild  23801  alexsublem  23987  alexsubALTlem4  23993  metrest  24468  dscopn  24517  reconnlem1  24771  cphsubrglem  25134  cphipval  25200  itgcnlem  25748  vieta1  26277  jensen  26956  2lgs  27375  nosep1o  27650  nodense  27661  bdayimaon  27662  conway  27768  etasslt  27782  slerec  27788  cofcutr  27889  om2noseqoi  28254  axlowdimlem6  28931  axlowdimlem7  28932  axlowdimlem16  28941  axlowdimlem17  28942  usgr2v1e2w  29236  0edg0rgr  29557  usgr2wlkspthlem2  29745  clwwlkf1  30035  0pthon  30113  ipval2  30693  sspg  30714  ssps  30716  sspmlem  30718  blocni  30791  ubthlem1  30856  bcsiALT  31165  ocsh  31269  chabs2  31503  pjoml6i  31575  osumcor2i  31630  nmopcoi  32081  opsqrlem6  32131  stlei  32226  mdslmd1lem1  32311  mdslmd2i  32316  atcvat3i  32382  atcvat4i  32383  sumdmdlem2  32405  dmdbr5ati  32408  xdivpnfrp  32912  fzo0pmtrlast  33108  tpr2rico  33948  ballotlemfp1  34529  ballotlemfc0  34530  ballotlemfcc  34531  ballotlemsup  34542  tgoldbachgt  34700  bnj545  34931  bnj548  34933  wevgblacfn  35136  satfv1  35390  trer  36339  filnetlem3  36403  filnetlem4  36404  phpreu  37633  matunitlindflem1  37645  poimirlem16  37665  poimirlem17  37666  poimirlem19  37668  poimirlem20  37669  poimirlem26  37675  mblfinlem1  37686  mblfinlem2  37687  mblfinlem3  37688  mblfinlem4  37689  ismblfin  37690  prter1  38902  pmapsub  39792  irrapx1  42826  dfacbasgrp  43107  dgraalem  43144  dgraaub  43147  onexlimgt  43242  cantnftermord  43319  oacl2g  43329  onmcl  43330  omabs2  43331  omcl2  43332  ofoaf  43354  naddwordnexlem3  43398  naddwordnexlem4  43400  brcoffn  44029  clsk3nimkb  44039  clsk1indlem1  44044  dvsconst  44329  dvsid  44330  dvsef  44331  islptre  45628  wallispilem1  46074  fourierdlem52  46167  ovnhoilem1  46610  gbowgt5  47756  gboge9  47758  nnsum3primesprm  47784  nnsum3primesgbe  47786  bgoldbnnsum3prm  47798  tgoldbachlt  47810  stgrnbgr0  47956  grlicref  47997  lincext1  48410  linds0  48421  lindsrng01  48424  lmod1lem3  48445  line2  48712  line2x  48714  inlinecirc02plem  48746  2oppf  49060  setrec1  49535