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  560  anabsi5  581  anim12dan  604  pm3.43  606  con3dimp  640  annimim  692  imnan  696  jaoian  802  jaodan  804  stdcndc  852  impidc  865  pm2.5gdc  873  con2bidc  882  pm5.18dc  890  dfandc  891  pm4.63dc  893  pm4.54dc  909  pm4.79dc  910  orcanai  935  annimdc  945  pm4.55dc  946  orandc  947  pm4.82  958  pm3.11dc  965  pm3.12dc  966  dn1dc  968  3jcad  1204  3expia  1231  3an1rs  1245  3imp1  1246  3imp2  1248  syl3anl2  1322  3jaoian  1341  3jaodan  1342  mp3anl1  1367  mp3anl2  1368  mp3anl3  1369  ecased  1385  xor3dc  1431  pm5.15dc  1433  xor2dc  1434  xornbidc  1435  xordc  1436  nbbndc  1438  biassdc  1439  bilukdc  1440  dfbi3dc  1441  pm5.24dc  1442  xordidc  1443  alanimi  1507  19.29  1668  equs4  1773  equsexd  1777  spimth  1783  equs5a  1842  ax11v2  1868  ax11b  1874  equs5or  1878  sb5rf  1900  equvin  1911  nfsb4t  2067  eu5  2127  mopick  2158  euexex  2165  2euswapdc  2171  exists2  2177  eqrdav  2230  dvelimdc  2395  nebidc  2482  pm13.18  2483  nelne1  2492  nelne2  2493  rspa  2580  ralrimdvv  2616  r19.21bi  2620  r19.26  2659  ralbi  2665  rexbi  2666  r19.29  2670  vtoclgft  2854  rspcva  2908  rspc2va  2924  elabgt  2947  eqeu  2976  mob2  2986  mob  2988  euind  2993  reu6  2995  reuind  3011  sbctt  3098  rspsbca  3116  sbcnestgf  3179  rspcsbela  3187  ssel2  3222  sselda  3227  sstr  3235  nssne1  3285  nssne2  3286  reuss2  3487  reupick  3491  reupick2  3493  reximdva0m  3510  ssn0  3537  disjel  3549  ssdisj  3551  absneu  3743  preqr1g  3849  prel12  3854  dfiun2g  4002  nbrne1  4107  nbrne2  4108  mpteq12f  4169  triun  4200  csbexga  4217  prcssprc  4230  iinexgm  4244  prexg  4301  copsex2t  4337  swopo  4403  poirr  4404  potr  4405  pofun  4409  issod  4416  ordelss  4476  trssord  4477  limelon  4496  trsuc  4519  eusvnfb  4551  rabxfrd  4566  regexmidlem1  4631  nordeq  4642  suc11g  4655  nnsuc  4714  brrelex12  4764  vtoclr  4774  optocl  4802  relop  4880  brcogw  4899  breldmg  4937  elreldm  4958  riinint  4993  issref  5119  xpidtr  5127  trin2  5128  cnveqb  5192  funopg  5360  funssres  5369  fununi  5398  funimass2  5408  imain  5412  fnun  5438  fco  5500  opelf  5507  f0rn0  5531  f1oun  5603  fun11iun  5604  fv3  5662  ndmfvg  5670  fvelima  5697  fvopab3ig  5720  fvmptssdm  5731  fvmptf  5739  fvimacnv  5762  fmptco  5813  fcof  5833  funfvima2  5887  funfvima3  5888  f1veqaeq  5910  f1ocnvfvrneq  5923  fliftfun  5937  isotr  5957  isoini  5959  isopolem  5963  isosolem  5965  moriotass  6002  acexmidlem2  6015  suppssfv  6231  suppssov1  6232  f1dmex  6278  releldm2  6348  f1o2ndf1  6393  poxp  6397  tposf2  6434  iunon  6450  smoel2  6469  tfrlem9  6485  tfrexlem  6500  tfr1onlembxssdm  6509  tfr1onlemres  6515  tfrcllembxssdm  6522  tfrcllemres  6528  tfrcl  6530  tfri3  6533  frecabcl  6565  sucinc2  6614  nnacom  6652  nnmcom  6657  nnsucsssuc  6660  nnsucuniel  6663  nntri2or2  6666  nnaordi  6676  nnmordi  6684  nnaordex  6696  nnm00  6698  ectocld  6770  iinerm  6776  th3qlem2  6807  elpm2r  6835  mapsncnv  6864  mptelixpg  6903  ixpsnf1o  6905  f1oen4g  6925  f1dom4g  6926  f1oen3g  6927  f1oeng  6930  en2d  6941  en3d  6942  dom2lem  6945  fundmen  6981  fundmeng  6982  unen  6991  modom  6994  rex2dom  6996  en2m  6999  xpdom2  7015  xpdom2g  7016  fopwdom  7022  nneneq  7043  phpm  7052  phpelm  7053  dif1enen  7069  fin0  7074  findcard  7077  diffifi  7083  ac6sfi  7087  onunsnss  7109  fiintim  7123  xpfi  7124  infidc  7133  fidcenum  7155  sbthlem1  7156  sbthlemi3  7158  sbthlemi10  7165  elfir  7172  isotilem  7205  inflbti  7223  ordiso2  7234  eldju2ndl  7271  eldju2ndr  7272  updjudhf  7278  mkvprop  7357  carden2bex  7394  pm54.43  7395  exmidfodomrlemeldju  7410  exmidfodomrlemreseldju  7411  exmidfodomrlemim  7412  pw1m  7442  ltmpig  7559  enq0sym  7652  addnq0mo  7667  mulnq0mo  7668  prarloclem3step  7716  prarloclem3  7717  genpml  7737  genpmu  7738  genprndl  7741  genprndu  7742  genpdisj  7743  distrlem1prl  7802  distrlem1pru  7803  distrlem4prl  7804  distrlem4pru  7805  distrlem5prl  7806  distrlem5pru  7807  ltsopr  7816  ltaddpr  7817  addcanprleml  7834  addcanprlemu  7835  recexprlemm  7844  recexprlemlol  7846  recexprlemupu  7848  aptiprleml  7859  aptiprlemu  7860  caucvgprlemnkj  7886  caucvgprlemnbj  7887  addsrmo  7963  mulsrmo  7964  srpospr  8003  caucvgsr  8022  axprecex  8100  mpomulf  8169  mulgt0  8254  ltne  8264  cnegexlem1  8354  cnegexlem2  8355  negf1o  8561  addgt0  8628  addgegt0  8629  addgtge0  8630  addge0  8631  recexre  8758  mulge0  8799  recexap  8833  prodgt02  9033  prodge02  9035  ltmul12a  9040  mulgt1  9043  nndivtr  9185  addltmul  9381  elnnnn0b  9446  xnn0nnn0pnf  9478  elnnz  9489  zmulcl  9533  nn0n0n1ge2  9550  nn0lt2  9561  nn0le2is012  9562  uzind2  9592  nn0ind-raph  9597  eluzp1m1  9780  uz3m2nn  9807  supinfneg  9829  infsupneg  9830  infregelbex  9832  negm  9849  lbzbi  9850  qaddcl  9869  qmulcl  9871  qreccl  9876  elpq  9883  ledivge1le  9961  nn0ledivnn  10002  xrltne  10048  xrre  10055  xrre2  10056  xrre3  10057  ge0gtmnf  10058  xltnegi  10070  xnn0xadd0  10102  xnegdi  10103  xposdif  10117  xlesubadd  10118  iccsupr  10201  icoshft  10225  icoshftf1o  10226  fznlem  10276  fzen  10278  uzsubsubfz  10282  fzsuc2  10314  elfz1b  10325  elfz0ubfz0  10360  elfz0fzfz0  10361  fz0fzelfz0  10362  fz0fzdiffz0  10365  elfzmlbp  10367  difelfznle  10370  nn0p1elfzo  10422  fzofzim  10428  elincfzoext  10439  eluzgtdifelfzo  10443  elfzodifsumelfzo  10447  elfzonlteqm1  10456  elfzom1p1elfzo  10460  ssfzo12bi  10471  subfzo0  10489  zsupcllemex  10491  zssinfcl  10493  exbtwnzlemstep  10508  modqmuladdnn0  10631  modfzo0difsn  10658  addmodlteq  10661  frec2uzlt2d  10667  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  seqf1og  10784  m1expcl2  10824  expge1  10839  leexp2r  10856  expubnd  10859  zesq  10921  expnlbnd  10927  nn0ltexp2  10972  nn0opthd  10985  faclbnd  11004  bcpasc  11029  hashprg  11073  seq3coll  11107  wrdnval  11148  wrdsymb0  11150  fstwrdne  11156  wrdred1hash  11161  swrdnd  11244  swrdwrdsymbg  11249  swrdsbslen  11251  swrdlsw  11254  swrdswrdlem  11289  swrdswrd  11290  pfxswrd  11291  cats1un  11306  wrd2ind  11308  swrdccatin1  11310  pfxccatin12lem4  11311  pfxccatin12lem2a  11312  pfxccatin12lem1  11313  swrdccatin2  11314  pfxccatin12lem2c  11315  pfxccatin12lem2  11316  pfxccatin12lem3  11317  pfxccatin12  11318  pfxccat3  11319  swrdccat  11320  pfxccat3a  11323  swrdccat3blem  11324  swrdccat3b  11325  swrdccatin2d  11329  reuccatpfxs1lem  11331  rexanuz  11566  rexuz3  11568  r19.29uz  11570  r19.2uz  11571  absnid  11651  leabs  11652  ltabs  11665  icodiamlt  11758  maxleast  11791  negfi  11806  climcn2  11887  climcau  11925  climcaucn  11929  sumdc  11936  fsum3cvg  11957  isumz  11968  fsumf1o  11969  fisumss  11971  isumss2  11972  fsumzcl2  11984  fsumsplit  11986  fsumsplitsnun  11998  sumsplitdc  12011  fsum2dlemstep  12013  telfsumo  12045  fsumparts  12049  fsumiun  12056  isumrpcl  12073  fproddccvg  12151  prod1dc  12165  prodssdc  12168  fprodssdc  12169  prodsnf  12171  fprodsplitdc  12175  fprod2dlemstep  12201  fprodmodd  12220  efexp  12261  efieq1re  12351  p1modz1  12373  dvds0lem  12380  dvds2ln  12403  dvdssub2  12414  dvdsadd2b  12419  dvdsabseq  12426  divconjdvds  12428  dvdsdivcl  12429  odd2np1  12452  oddge22np1  12460  opoe  12474  omoe  12475  opeo  12476  omeo  12477  m1expo  12479  nn0ehalf  12482  nn0o1gt2  12484  nno  12485  divalgb  12504  ndvdsadd  12510  bitsinv1lem  12540  gcd0id  12568  gcdneg  12571  gcdaddm  12573  bezoutlemstep  12586  dfgcd2  12603  gcddiv  12608  dvdsmulgcd  12614  bezoutr  12621  bezoutr1  12622  uzwodc  12626  nninfctlemfo  12629  algfx  12642  lcmgcdlem  12667  lcmgcdeq  12673  coprmdvds  12682  divgcdcoprmex  12692  cncongr1  12693  cncongr2  12694  isprm3  12708  dvdsnprmd  12715  prmgt1  12722  oddprmgt2  12724  isprm6  12737  cncongrprm  12747  phibndlem  12806  phimullem  12815  powm2modprm  12843  modprm0  12845  modprmn0modprm0  12847  prm23lt5  12854  pcneg  12916  pcprmpw2  12924  dvdsprmpweqnn  12927  dvdsprmpweqle  12928  pcaddlem  12930  fldivp1  12939  pcfac  12941  oddprmdvds  12945  prmunb  12953  ennnfone  13064  unct  13081  lidrididd  13483  gsummgmpropd  13495  sgrpass  13509  issgrpd  13513  issubmnd  13543  imasmnd2  13553  mnd1id  13557  insubm  13586  dfgrp2  13628  grpid  13640  grpasscan1  13664  dfgrp3mlem  13699  dfgrp3me  13701  imasgrp2  13715  mulgnn0gsum  13733  mulgnn0p1  13738  mulgaddcom  13751  mulginvcom  13752  mulgass  13764  mulgpropdg  13769  subginv  13786  issubg2m  13794  issubg4m  13798  grpissubg  13799  resgrpisgrp  13800  subgintm  13803  kerf1ghm  13879  cmncom  13907  imasabl  13941  rngdi  13972  rngdir  13973  rngpropd  13987  imasrng  13988  imasring  14096  nzrunit  14221  issubrng2  14243  subrngintm  14245  issubrg2  14274  subrgintm  14276  lmodfopnelem1  14357  lmodfopnelem2  14358  lmodfopne  14359  islssm  14390  islidlm  14512  rnglidlmcl  14513  dflidl2rng  14514  rnglidlmmgm  14529  rnglidlmsgrp  14530  rnglidlrng  14531  dvdsrzring  14636  znidom  14690  uniopn  14744  istopon  14756  fiinbas  14792  tg2  14803  tgcl  14807  0nnei  14896  tgrest  14912  tgcn  14951  cnpnei  14962  cncnp2m  14974  lmtopcnp  14993  tx2cn  15013  txcn  15018  cnmpt21  15034  isxmet2d  15091  metrest  15249  metcnpi3  15260  tgioo  15297  fsumcncntop  15310  elcncf1di  15322  climcncf  15327  cncfco  15334  suplociccreex  15367  cnplimcim  15410  cnlimci  15416  reeff1olem  15514  efltlemlt  15517  zabsle1  15747  lgslem3  15750  lgsmod  15774  lgsdir2lem5  15780  lgsdir2  15781  lgsne0  15786  lgsdirnn0  15795  gausslemma2dlem0f  15802  gausslemma2dlem1a  15806  gausslemma2dlem3  15811  2lgslem1c  15838  2lgslem3a1  15845  2lgslem3b1  15846  2lgslem3c1  15847  2lgslem3d1  15848  2lgslem3  15849  2lgsoddprmlem2  15854  uhgrm  15948  incistruhgr  15960  upgrfnen  15968  umgrfnen  15978  umgrnloop  15986  upgredgpr  16019  usgrausgrben  16042  usgredgop  16043  usgruspgrben  16056  usgrislfuspgrdom  16060  umgrvad2edg  16081  ushgredgedg  16096  ushgredgedgloop  16098  uhgr0v0e  16104  subgreldmiedg  16139  subupgr  16143  uhgrspansubgrlem  16146  vtxdg0v  16164  wlkpropg  16194  wlkvg  16198  wlkl1loop  16228  upgriswlkdc  16230  upgrwlkedg  16231  upgrwlkvtxedg  16234  uspgr2wlkeq  16235  wlkres  16249  trlf1  16258  clwwlk1loop  16269  clwwlkccatlem  16270  isclwwlknx  16286  clwwlkn1loopb  16290  clwwlkext2edg  16292  umgr2cwwk2dif  16294  clwwlknonex2lem2  16308  clwwlknonex2  16309  eupthseg  16322  eupth2lem3lem4fi  16343  bj-charfun  16453  bj-charfunr  16456  bj-charfunbi  16457  bj-prexg  16557  peano5set  16586  bj-peano4  16601  bj-nn0suc  16610  bj-nn0sucALT  16624  bj-findis  16625  exmidsbthrlem  16677  trilpolemres  16697  trirec0  16699  nconstwlpolem  16721  neapmkv  16724  gfsumval  16732