Theorem imp 124

Description: Importation inference. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Eric Schmidt, 22-Dec-2006.)

Hypothesis

Ref	Expression
imp.1	|- ( ph -> ( ps -> ch ) )

Assertion

Ref	Expression
imp	|- ( ( ph /\ ps ) -> ch )

Proof of Theorem imp

Step	Hyp	Ref	Expression
1		simpl 109	. 2 |- ( ( ph /\ ps ) -> ph )
2		simpr 110	. 2 |- ( ( ph /\ ps ) -> ps )
3		imp.1	. 2 |- ( ph -> ( ps -> ch ) )
4	1, 2, 3	sylc 62	1 |- ( ( ph /\ ps ) -> ch )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem is referenced by:  impcom  125  impd  254  imp31  256  imp32  257  expdimp  259  impancom  260  pm3.22  265  ancoms  268  adantr  276  impel  280  biimpa  296  biimpar  297  biimpac  298  biimparc  299  pm3.33  345  pm3.34  346  pm3.35  347  pm5.31  348  imp4b  350  imp41  353  imp42  354  imp43  355  imp44  356  imp45  357  imp5g  360  expr  375  impac  381  sylan9  409  sylan9r  410  imdistani  445  mpan10  474  adantl4r  517  adantl5r  525  adantl6r  526  a2and  558  anabsi5  579  anim12dan  600  pm3.43  602  con3dimp  636  annimim  687  imnan  691  jaoian  796  jaodan  798  stdcndc  846  impidc  859  pm2.5gdc  867  con2bidc  876  pm5.18dc  884  dfandc  885  pm4.63dc  887  pm4.54dc  903  pm4.79dc  904  orcanai  929  annimdc  939  pm4.55dc  940  orandc  941  pm4.82  952  pm3.11dc  959  pm3.12dc  960  dn1dc  962  3jcad  1180  3expia  1207  3an1rs  1221  3imp1  1222  3imp2  1224  syl3anl2  1298  3jaoian  1317  3jaodan  1318  mp3anl1  1343  mp3anl2  1344  mp3anl3  1345  ecased  1361  xor3dc  1406  pm5.15dc  1408  xor2dc  1409  xornbidc  1410  xordc  1411  nbbndc  1413  biassdc  1414  bilukdc  1415  dfbi3dc  1416  pm5.24dc  1417  xordidc  1418  alanimi  1481  19.29  1642  equs4  1747  equsexd  1751  spimth  1757  equs5a  1816  ax11v2  1842  ax11b  1848  equs5or  1852  sb5rf  1874  equvin  1885  nfsb4t  2041  eu5  2100  mopick  2131  euexex  2138  2euswapdc  2144  exists2  2150  eqrdav  2203  dvelimdc  2368  nebidc  2455  pm13.18  2456  nelne1  2465  nelne2  2466  rspa  2553  ralrimdvv  2589  r19.21bi  2593  r19.26  2631  ralbi  2637  rexbi  2638  r19.29  2642  vtoclgft  2822  rspcva  2874  rspc2va  2890  elabgt  2913  eqeu  2942  mob2  2952  mob  2954  euind  2959  reu6  2961  reuind  2977  sbctt  3064  rspsbca  3081  sbcnestgf  3144  rspcsbela  3152  ssel2  3187  sselda  3192  sstr  3200  nssne1  3250  nssne2  3251  reuss2  3452  reupick  3456  reupick2  3458  reximdva0m  3475  ssn0  3502  disjel  3514  ssdisj  3516  absneu  3704  preqr1g  3806  prel12  3811  dfiun2g  3958  nbrne1  4062  nbrne2  4063  mpteq12f  4123  triun  4154  csbexga  4171  iinexgm  4197  prexg  4254  copsex2t  4288  swopo  4352  poirr  4353  potr  4354  pofun  4358  issod  4365  ordelss  4425  trssord  4426  limelon  4445  trsuc  4468  eusvnfb  4500  rabxfrd  4515  regexmidlem1  4580  nordeq  4591  suc11g  4604  nnsuc  4663  brrelex12  4712  vtoclr  4722  optocl  4750  relop  4827  brcogw  4846  breldmg  4883  elreldm  4903  riinint  4938  issref  5064  xpidtr  5072  trin2  5073  cnveqb  5137  funopg  5304  funssres  5312  fununi  5341  funimass2  5351  imain  5355  fnun  5381  fco  5440  opelf  5446  f0rn0  5469  f1oun  5541  fun11iun  5542  fv3  5598  ndmfvg  5606  fvelima  5629  fvopab3ig  5652  fvmptssdm  5663  fvmptf  5671  fvimacnv  5694  fmptco  5745  funfvima2  5816  funfvima3  5817  f1veqaeq  5837  f1ocnvfvrneq  5850  fliftfun  5864  isotr  5884  isoini  5886  isopolem  5890  isosolem  5892  moriotass  5927  acexmidlem2  5940  suppssfv  6153  suppssov1  6154  f1dmex  6200  releldm2  6270  f1o2ndf1  6313  poxp  6317  tposf2  6353  iunon  6369  smoel2  6388  tfrlem9  6404  tfrexlem  6419  tfr1onlembxssdm  6428  tfr1onlemres  6434  tfrcllembxssdm  6441  tfrcllemres  6447  tfrcl  6449  tfri3  6452  frecabcl  6484  sucinc2  6531  nnacom  6569  nnmcom  6574  nnsucsssuc  6577  nnsucuniel  6580  nntri2or2  6583  nnaordi  6593  nnmordi  6601  nnaordex  6613  nnm00  6615  ectocld  6687  iinerm  6693  th3qlem2  6724  elpm2r  6752  mapsncnv  6781  mptelixpg  6820  ixpsnf1o  6822  f1oen4g  6842  f1dom4g  6843  f1oen3g  6844  f1oeng  6847  en2d  6858  en3d  6859  dom2lem  6862  fundmen  6897  fundmeng  6898  unen  6907  rex2dom  6909  xpdom2  6925  xpdom2g  6926  fopwdom  6932  nneneq  6953  phpm  6961  phpelm  6962  dif1enen  6976  fin0  6981  findcard  6984  diffifi  6990  ac6sfi  6994  onunsnss  7013  fiintim  7027  xpfi  7028  infidc  7035  fidcenum  7057  sbthlem1  7058  sbthlemi3  7060  sbthlemi10  7067  elfir  7074  isotilem  7107  inflbti  7125  ordiso2  7136  eldju2ndl  7173  eldju2ndr  7174  updjudhf  7180  mkvprop  7259  carden2bex  7296  pm54.43  7297  exmidfodomrlemeldju  7306  exmidfodomrlemreseldju  7307  exmidfodomrlemim  7308  ltmpig  7451  enq0sym  7544  addnq0mo  7559  mulnq0mo  7560  prarloclem3step  7608  prarloclem3  7609  genpml  7629  genpmu  7630  genprndl  7633  genprndu  7634  genpdisj  7635  distrlem1prl  7694  distrlem1pru  7695  distrlem4prl  7696  distrlem4pru  7697  distrlem5prl  7698  distrlem5pru  7699  ltsopr  7708  ltaddpr  7709  addcanprleml  7726  addcanprlemu  7727  recexprlemm  7736  recexprlemlol  7738  recexprlemupu  7740  aptiprleml  7751  aptiprlemu  7752  caucvgprlemnkj  7778  caucvgprlemnbj  7779  addsrmo  7855  mulsrmo  7856  srpospr  7895  caucvgsr  7914  axprecex  7992  mpomulf  8061  mulgt0  8146  ltne  8156  cnegexlem1  8246  cnegexlem2  8247  negf1o  8453  addgt0  8520  addgegt0  8521  addgtge0  8522  addge0  8523  recexre  8650  mulge0  8691  recexap  8725  prodgt02  8925  prodge02  8927  ltmul12a  8932  mulgt1  8935  nndivtr  9077  addltmul  9273  elnnnn0b  9338  xnn0nnn0pnf  9370  elnnz  9381  zmulcl  9425  nn0n0n1ge2  9442  nn0lt2  9453  nn0le2is012  9454  uzind2  9484  nn0ind-raph  9489  eluzp1m1  9671  uz3m2nn  9693  supinfneg  9715  infsupneg  9716  infregelbex  9718  negm  9735  lbzbi  9736  qaddcl  9755  qmulcl  9757  qreccl  9762  elpq  9769  ledivge1le  9847  nn0ledivnn  9888  xrltne  9934  xrre  9941  xrre2  9942  xrre3  9943  ge0gtmnf  9944  xltnegi  9956  xnn0xadd0  9988  xnegdi  9989  xposdif  10003  xlesubadd  10004  iccsupr  10087  icoshft  10111  icoshftf1o  10112  fznlem  10162  fzen  10164  uzsubsubfz  10168  fzsuc2  10200  elfz1b  10211  elfz0ubfz0  10246  elfz0fzfz0  10247  fz0fzelfz0  10248  fz0fzdiffz0  10251  elfzmlbp  10253  difelfznle  10256  fzofzim  10310  elincfzoext  10320  eluzgtdifelfzo  10324  elfzodifsumelfzo  10328  elfzonlteqm1  10337  elfzom1p1elfzo  10341  ssfzo12bi  10352  subfzo0  10369  zsupcllemex  10371  zssinfcl  10373  exbtwnzlemstep  10388  modqmuladdnn0  10511  modfzo0difsn  10538  addmodlteq  10541  frec2uzlt2d  10547  frecuzrdgtcl  10555  frecuzrdgfunlem  10562  seqf1og  10664  m1expcl2  10704  expge1  10719  leexp2r  10736  expubnd  10739  zesq  10801  expnlbnd  10807  nn0ltexp2  10852  nn0opthd  10865  faclbnd  10884  bcpasc  10909  hashprg  10951  seq3coll  10985  wrdnval  11022  wrdsymb0  11024  fstwrdne  11030  wrdred1hash  11035  rexanuz  11270  rexuz3  11272  r19.29uz  11274  r19.2uz  11275  absnid  11355  leabs  11356  ltabs  11369  icodiamlt  11462  maxleast  11495  negfi  11510  climcn2  11591  climcau  11629  climcaucn  11633  sumdc  11640  fsum3cvg  11660  isumz  11671  fsumf1o  11672  fisumss  11674  isumss2  11675  fsumzcl2  11687  fsumsplit  11689  fsumsplitsnun  11701  sumsplitdc  11714  fsum2dlemstep  11716  telfsumo  11748  fsumparts  11752  fsumiun  11759  isumrpcl  11776  fproddccvg  11854  prod1dc  11868  prodssdc  11871  fprodssdc  11872  prodsnf  11874  fprodsplitdc  11878  fprod2dlemstep  11904  fprodmodd  11923  efexp  11964  efieq1re  12054  p1modz1  12076  dvds0lem  12083  dvds2ln  12106  dvdssub2  12117  dvdsadd2b  12122  dvdsabseq  12129  divconjdvds  12131  dvdsdivcl  12132  odd2np1  12155  oddge22np1  12163  opoe  12177  omoe  12178  opeo  12179  omeo  12180  m1expo  12182  nn0ehalf  12185  nn0o1gt2  12187  nno  12188  divalgb  12207  ndvdsadd  12213  bitsinv1lem  12243  gcd0id  12271  gcdneg  12274  gcdaddm  12276  bezoutlemstep  12289  dfgcd2  12306  gcddiv  12311  dvdsmulgcd  12317  bezoutr  12324  bezoutr1  12325  uzwodc  12329  nninfctlemfo  12332  algfx  12345  lcmgcdlem  12370  lcmgcdeq  12376  coprmdvds  12385  divgcdcoprmex  12395  cncongr1  12396  cncongr2  12397  isprm3  12411  dvdsnprmd  12418  prmgt1  12425  oddprmgt2  12427  isprm6  12440  cncongrprm  12450  phibndlem  12509  phimullem  12518  powm2modprm  12546  modprm0  12548  modprmn0modprm0  12550  prm23lt5  12557  pcneg  12619  pcprmpw2  12627  dvdsprmpweqnn  12630  dvdsprmpweqle  12631  pcaddlem  12633  fldivp1  12642  pcfac  12644  oddprmdvds  12648  prmunb  12656  ennnfone  12767  unct  12784  lidrididd  13185  gsummgmpropd  13197  sgrpass  13211  issgrpd  13215  issubmnd  13245  imasmnd2  13255  mnd1id  13259  insubm  13288  dfgrp2  13330  grpid  13342  grpasscan1  13366  dfgrp3mlem  13401  dfgrp3me  13403  imasgrp2  13417  mulgnn0gsum  13435  mulgnn0p1  13440  mulgaddcom  13453  mulginvcom  13454  mulgass  13466  mulgpropdg  13471  subginv  13488  issubg2m  13496  issubg4m  13500  grpissubg  13501  resgrpisgrp  13502  subgintm  13505  kerf1ghm  13581  cmncom  13609  imasabl  13643  rngdi  13673  rngdir  13674  rngpropd  13688  imasrng  13689  imasring  13797  nzrunit  13921  issubrng2  13943  subrngintm  13945  issubrg2  13974  subrgintm  13976  lmodfopnelem1  14057  lmodfopnelem2  14058  lmodfopne  14059  islssm  14090  islidlm  14212  rnglidlmcl  14213  dflidl2rng  14214  rnglidlmmgm  14229  rnglidlmsgrp  14230  rnglidlrng  14231  dvdsrzring  14336  znidom  14390  uniopn  14444  istopon  14456  fiinbas  14492  tg2  14503  tgcl  14507  0nnei  14596  tgrest  14612  tgcn  14651  cnpnei  14662  cncnp2m  14674  lmtopcnp  14693  tx2cn  14713  txcn  14718  cnmpt21  14734  isxmet2d  14791  metrest  14949  metcnpi3  14960  tgioo  14997  fsumcncntop  15010  elcncf1di  15022  climcncf  15027  cncfco  15034  suplociccreex  15067  cnplimcim  15110  cnlimci  15116  reeff1olem  15214  efltlemlt  15217  zabsle1  15447  lgslem3  15450  lgsmod  15474  lgsdir2lem5  15480  lgsdir2  15481  lgsne0  15486  lgsdirnn0  15495  gausslemma2dlem0f  15502  gausslemma2dlem1a  15506  gausslemma2dlem3  15511  2lgslem1c  15538  2lgslem3a1  15545  2lgslem3b1  15546  2lgslem3c1  15547  2lgslem3d1  15548  2lgslem3  15549  2lgsoddprmlem2  15554  bj-charfun  15705  bj-charfunr  15708  bj-charfunbi  15709  bj-prexg  15809  peano5set  15838  bj-peano4  15853  bj-nn0suc  15862  bj-nn0sucALT  15876  bj-findis  15877  exmidsbthrlem  15923  trilpolemres  15943  trirec0  15945  nconstwlpolem  15966  neapmkv  15969