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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem is used 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  413  sylan9r  414  imdistani  449  mpan10  478  adantl4r  521  adantl5r  529  adantl6r  530  a2and  564  anabsi5  585  anim12dan  608  pm3.43  610  con3dimp  644  annimim  697  imnan  701  jaoian  807  jaodan  809  stdcndc  857  impidc  870  pm2.5gdc  878  con2bidc  887  pm5.18dc  895  dfandc  896  pm4.63dc  898  pm4.54dc  914  pm4.79dc  915  orcanai  940  annimdc  950  pm4.55dc  951  orandc  952  pm4.82  963  pm3.11dc  970  pm3.12dc  971  dn1dc  973  3jcad  1209  3expia  1236  3an1rs  1250  3imp1  1251  3imp2  1253  syl3anl2  1327  3jaoian  1346  3jaodan  1347  mp3anl1  1372  mp3anl2  1373  mp3anl3  1374  ecased  1390  xor3dc  1436  pm5.15dc  1438  xor2dc  1439  xornbidc  1440  xordc  1441  nbbndc  1443  biassdc  1444  bilukdc  1445  dfbi3dc  1446  pm5.24dc  1447  xordidc  1448  alanimi  1512  19.29  1673  equs4  1777  equsexd  1782  spimth  1788  equs5a  1847  ax11v2  1873  ax11b  1879  equs5or  1883  sb5rf  1905  equvin  1916  nfsb4t  2074  eu5  2134  mopick  2165  euexex  2172  2euswapdc  2178  exists2  2184  eqrdav  2237  dvelimdc  2413  nebidc  2500  pm13.18  2501  nelne1  2510  nelne2  2511  rspa  2598  ralrimdvv  2634  r19.21bi  2638  r19.26  2677  ralbi  2683  rexbi  2684  r19.29  2688  vtoclgft  2873  rspcva  2927  rspc2va  2944  elabgt  2967  eqeu  2996  mob2  3006  mob  3008  euind  3013  reu6  3015  reuind  3031  sbctt  3118  rspsbca  3136  sbcnestgf  3199  rspcsbela  3207  ssel2  3243  sselda  3248  sstr  3256  nssne1  3306  nssne2  3307  reuss2  3513  reupick  3517  reupick2  3519  reximdva0m  3537  ssn0  3566  disjel  3579  ssdisj  3581  ifeqeqxdc  3687  absneu  3783  preqr1g  3891  prel12  3896  dfiun2g  4044  nbrne1  4150  nbrne2  4151  mpteq12f  4212  triun  4244  csbexga  4263  prcssprc  4276  iinexgm  4292  prexg  4351  copsex2t  4387  swopo  4453  poirr  4454  potr  4455  pofun  4459  issod  4466  ordelss  4526  trssord  4527  limelon  4546  trsuc  4569  eusvnfb  4602  rabxfrd  4617  regexmidlem1  4682  nordeq  4693  suc11g  4706  nnsuc  4765  brrelex12  4815  vtoclr  4825  optocl  4853  relop  4932  brcogw  4951  breldmg  4989  elreldm  5010  riinint  5045  xpexcnvm  5145  issref  5173  xpidtr  5181  trin2  5182  cnveqb  5246  funopg  5414  funssres  5423  fununi  5452  funimass2  5462  imain  5466  fnun  5492  fco  5555  opelf  5563  f0rn0  5590  f1oun  5662  fun11iun  5663  fv3  5721  ndmfvg  5729  fvelima  5757  fvopab3ig  5782  fvmptssdm  5793  fvmptf  5801  fvimacnv  5827  fmptco  5877  fcof  5897  funfvima2  5954  funfvima3  5955  f1veqaeq  5978  f1ocnvfvrneq  5991  fliftfun  6005  isotr  6025  isoini  6027  isopolem  6031  isosolem  6033  moriotass  6072  acexmidlem2  6085  suppssov1  6302  f1dmex  6349  elabreximd  6360  releldm2  6423  f1o2ndf1  6468  poxp  6472  fsuppeq  6491  suppssfvg  6507  tposf2  6544  iunon  6560  smoel2  6579  tfrlem9  6595  tfrexlem  6610  tfr1onlembxssdm  6619  tfr1onlemres  6625  tfrcllembxssdm  6632  tfrcllemres  6638  tfrcl  6640  tfri3  6643  frecabcl  6675  sucinc2  6724  nnacom  6762  nnmcom  6767  nnsucsssuc  6770  nnsucuniel  6773  nntri2or2  6776  nnaordi  6786  nnmordi  6794  nnaordex  6806  nnm00  6808  ectocld  6880  iinerm  6886  th3qlem2  6917  elpm2r  6945  mapsnd  6976  mapsncnv  6983  mptelixpg  7022  ixpsnf1o  7024  f1oen4g  7044  f1dom4g  7045  f1oen3g  7046  f1oeng  7049  en2d  7060  en3d  7061  dom2lem  7064  fundmen  7100  fundmeng  7101  unen  7111  modom  7114  rex2dom  7116  en2m  7119  xpdom2  7135  xpdom2g  7136  fopwdom  7142  nneneq  7164  phpm  7173  phpelm  7174  dif1enen  7190  fin0  7195  findcard  7198  diffifi  7204  ac6sfi  7208  onunsnss  7230  fiintim  7244  xpfi  7245  infidc  7254  fidcenum  7280  sbthlem1  7281  sbthlemi3  7283  sbthlemi10  7290  elfir  7312  isotilem  7352  inflbti  7370  ordiso2  7381  eldju2ndl  7418  eldju2ndr  7419  updjudhf  7425  mkvprop  7504  carden2bex  7541  pm54.43  7542  exmidfodomrlemeldju  7557  exmidfodomrlemreseldju  7558  exmidfodomrlemim  7559  pw1m  7589  ltmpig  7712  enq0sym  7805  addnq0mo  7820  mulnq0mo  7821  prarloclem3step  7869  prarloclem3  7870  genpml  7890  genpmu  7891  genprndl  7894  genprndu  7895  genpdisj  7896  distrlem1prl  7955  distrlem1pru  7956  distrlem4prl  7957  distrlem4pru  7958  distrlem5prl  7959  distrlem5pru  7960  ltsopr  7969  ltaddpr  7970  addcanprleml  7987  addcanprlemu  7988  recexprlemm  7997  recexprlemlol  7999  recexprlemupu  8001  aptiprleml  8012  aptiprlemu  8013  caucvgprlemnkj  8039  caucvgprlemnbj  8040  addsrmo  8116  mulsrmo  8117  srpospr  8156  caucvgsr  8175  axprecex  8253  mpomulf  8322  mulgt0  8406  ltne  8416  cnegexlem1  8508  cnegexlem2  8509  negf1o  8716  addgt0  8783  addgegt0  8784  addgtge0  8785  addge0  8786  recexre  8914  mulge0  8955  recexap  8989  prodgt02  9191  prodge02  9193  ltmul12a  9198  mulgt1  9201  nndivtr  9355  addltmul  9553  elnnnn0b  9618  fcdmnn0supp  9626  fcdmnn0suppg  9627  xnn0nnn0pnf  9652  elnnz  9663  zmulcl  9707  nn0n0n1ge2  9724  nn0lt2  9736  nn0le2is012  9737  uzind2  9768  nn0ind-raph  9773  eluzp1m1  9961  uz3m2nn  9988  supinfneg  10010  infsupneg  10011  infregelbex  10013  negm  10030  lbzbi  10031  qaddcl  10050  qmulcl  10052  qreccl  10057  elpq  10065  ledivge1le  10143  nn0ledivnn  10184  xrltne  10231  xrre  10238  xrre2  10239  xrre3  10240  ge0gtmnf  10241  xltnegi  10253  xnn0xadd0  10285  xnegdi  10286  xposdif  10300  xlesubadd  10301  iccsupr  10384  icoshft  10408  icoshftf1o  10409  fznlem  10461  fzen  10463  uzsubsubfz  10468  fzsuc2  10502  elfz1b  10513  elfz0ubfz0  10548  elfz0fzfz0  10549  fz0fzelfz0  10550  fz0fzdiffz0  10553  elfzmlbp  10555  difelfznle  10558  nn0p1elfzo  10610  fzofzim  10616  elincfzoext  10627  eluzgtdifelfzo  10631  elfzodifsumelfzo  10635  elfzonlteqm1  10644  elfzom1p1elfzo  10648  ssfzo12bi  10659  subfzo0  10677  zsupcllemex  10679  zssinfcl  10681  exbtwnzlemstep  10698  modqmuladdnn0  10825  modfzo0difsn  10852  addmodlteq  10855  frec2uzlt2d  10861  frecuzrdgtcl  10869  frecuzrdgfunlem  10876  seqf1og  10978  m1expcl2  11018  expge1  11033  leexp2r  11050  expubnd  11053  zesq  11116  expnlbnd  11122  nn0ltexp2  11168  nn0opthd  11181  faclbnd  11200  bcpasc  11225  hashprg  11270  hashf1  11308  seq3coll  11315  wrdnval  11356  wrdsymb0  11358  fstwrdne  11364  wrdred1hash  11369  swrdnd  11452  swrdwrdsymbg  11457  swrdsbslen  11459  swrdlsw  11462  swrdswrdlem  11497  swrdswrd  11498  pfxswrd  11499  cats1un  11514  wrd2ind  11516  swrdccatin1  11518  pfxccatin12lem4  11519  pfxccatin12lem2a  11520  pfxccatin12lem1  11521  swrdccatin2  11522  pfxccatin12lem2c  11523  pfxccatin12lem2  11524  pfxccatin12lem3  11525  pfxccatin12  11526  pfxccat3  11527  swrdccat  11528  pfxccat3a  11531  swrdccat3blem  11532  swrdccat3b  11533  swrdccatin2d  11537  reuccatpfxs1lem  11539  rexanuz  11775  rexuz3  11777  r19.29uz  11779  r19.2uz  11780  absnid  11860  leabs  11861  ltabs  11875  icodiamlt  11968  maxleast  12001  negfi  12016  climcn2  12099  climcau  12137  climcaucn  12141  sumdc  12148  fsum3cvg  12169  isumz  12180  fsumf1o  12181  fisumss  12183  isumss2  12184  fsumzcl2  12196  fsumsplit  12198  fsumsplitsnun  12210  sumsplitdc  12223  fsum2dlemstep  12225  telfsumo  12257  fsumparts  12261  fsumiun  12268  isumrpcl  12285  fproddccvg  12363  prod1dc  12377  prodssdc  12380  fprodssdc  12381  prodsnf  12383  fprodsplitdc  12387  fprod2dlemstep  12413  fprodmodd  12432  efexp  12473  efieq1re  12563  p1modz1  12585  dvds0lem  12592  dvds2ln  12615  dvdssub2  12626  dvdsadd2b  12631  dvdsabseq  12638  divconjdvds  12640  dvdsdivcl  12641  odd2np1  12664  oddge22np1  12672  opoe  12686  omoe  12687  opeo  12688  omeo  12689  m1expo  12691  nn0ehalf  12694  nn0o1gt2  12696  nno  12697  divalgb  12716  ndvdsadd  12722  bitsinv1lem  12752  gcd0id  12780  gcdneg  12783  gcdaddm  12785  bezoutlemstep  12798  dfgcd2  12815  gcddiv  12820  dvdsmulgcd  12826  bezoutr  12833  bezoutr1  12834  uzwodc  12838  nninfctlemfo  12841  algfx  12854  lcmgcdlem  12879  lcmgcdeq  12885  coprmdvds  12894  divgcdcoprmex  12904  cncongr1  12905  cncongr2  12906  isprm3  12920  dvdsnprmd  12927  prmgt1  12935  oddprmgt2  12937  isprm6  12950  cncongrprm  12960  phibndlem  13022  phimullem  13031  powm2modprm  13059  modprm0  13061  modprmn0modprm0  13063  prm23lt5  13070  pcneg  13132  pcprmpw2  13140  dvdsprmpweqnn  13143  dvdsprmpweqle  13144  pcaddlem  13146  fldivp1  13155  pcfac  13157  oddprmdvds  13161  prmunb  13169  ballotfilemfc0  13289  ballotfilemfcc  13290  ballotfilem4  13298  ballotfilemi1  13302  ballotfilemii  13303  ballotfilemic  13307  ballotfilem1c  13308  ballotfilemirc  13332  ballotfilem7  13336  ennnfone  13373  unct  13390  lidrididd  13760  sgrpass  13781  issgrpd  13785  issubmnd  13813  imasmnd2  13817  mnd1id  13821  insubm  13850  dfgrp2  13890  grpid  13902  grpasscan1  13926  dfgrp3mlem  13961  dfgrp3me  13963  imasgrp2  13971  mulgnn0gzsum  13989  mulgnn0p1  13994  mulgaddcom  14007  mulginvcom  14008  mulgass  14020  mulgpropdg  14025  subginv  14042  issubg2m  14050  issubg4m  14054  grpissubg  14055  resgrpisgrp  14056  subgintm  14059  kerf1ghm  14135  cmncom  14194  imasabl  14229  gsumvalfi  14241  rngdi  14345  rngdir  14346  rngpropd  14360  imasrng  14361  rng1zrlem  14364  imasring  14477  nzrunit  14603  issubrng2  14626  subrngintm  14628  issubrg2  14657  subrgintm  14659  lmodfopnelem1  14769  lmodfopnelem2  14770  lmodfopne  14771  islssm  14802  islidlm  14924  rnglidlmcl  14925  dflidl2rng  14926  rnglidlmmgm  14941  rnglidlmsgrp  14942  rnglidlrng  14943  gsumfsum  15031  dvdsrzring  15046  znidom  15100  issubassa3  15120  assamulgscmlem2  15150  psrbagmaxlem1  15178  uniopn  15244  istopon  15256  fiinbas  15292  tg2  15303  tgcl  15307  0nnei  15396  tgrest  15412  tgcn  15451  cnpnei  15462  cncnp2m  15474  lmtopcnp  15493  tx2cn  15513  txcn  15518  cnmpt21  15534  isxmet2d  15591  metrest  15749  metcnpi3  15760  tgioo  15797  fsumcncntop  15810  elcncf1di  15822  climcncf  15827  cncfco  15834  suplociccreex  15867  cnplimcim  15910  cnlimci  15916  reeff1olem  16014  efltlemlt  16017  efap1p  16022  sineq0re  16093  pellexlem1  16246  chtqub  16313  bpos1  16327  bposlem6  16333  zabsle1  16340  lgslem3  16343  lgsmod  16367  lgsdir2lem5  16373  lgsdir2  16374  lgsne0  16379  lgsdirnn0  16388  gausslemma2dlem0f  16395  gausslemma2dlem1a  16399  gausslemma2dlem3  16404  2lgslem1c  16431  2lgslem3a1  16438  2lgslem3b1  16439  2lgslem3c1  16440  2lgslem3d1  16441  2lgslem3  16442  2lgsoddprmlem2  16447  uhgrm  16541  incistruhgr  16553  upgrfnen  16561  umgrfnen  16571  umgrnloop  16579  upgredgpr  16612  usgrausgrben  16635  usgredgop  16636  usgruspgrben  16649  usgrislfuspgrdom  16653  umgrvad2edg  16674  ushgredgedg  16689  ushgredgedgloop  16691  uhgr0v0e  16697  subgreldmiedg  16732  subupgr  16736  uhgrspansubgrlem  16739  vtxdg0v  16757  wlkpropg  16787  wlkvg  16791  wlkl1loop  16821  upgriswlkdc  16823  upgrwlkedg  16824  upgrwlkvtxedg  16827  uspgr2wlkeq  16828  wlkres  16842  trlf1  16851  clwwlk1loop  16862  clwwlkccatlem  16863  isclwwlknx  16879  clwwlkn1loopb  16883  clwwlkext2edg  16885  umgr2cwwk2dif  16887  clwwlknonex2lem2  16901  clwwlknonex2  16902  eupthseg  16915  eupth2lem3lem4fi  16936  bj-charfun  17055  bj-charfunr  17058  bj-charfunbi  17059  bj-prexg  17159  peano5set  17188  bj-peano4  17203  bj-nn0suc  17212  bj-nn0sucALT  17226  bj-findis  17227  exmidsbthrlem  17290  trilpolemres  17315  trirec0  17317  nconstwlpolem  17339  neapmkv  17342  alsex  17363  ralsex  17364  als-no-surprise  17371