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  6543  iunon  6559  smoel2  6578  tfrlem9  6594  tfrexlem  6609  tfr1onlembxssdm  6618  tfr1onlemres  6624  tfrcllembxssdm  6631  tfrcllemres  6637  tfrcl  6639  tfri3  6642  frecabcl  6674  sucinc2  6723  nnacom  6761  nnmcom  6766  nnsucsssuc  6769  nnsucuniel  6772  nntri2or2  6775  nnaordi  6785  nnmordi  6793  nnaordex  6805  nnm00  6807  ectocld  6879  iinerm  6885  th3qlem2  6916  elpm2r  6944  mapsnd  6974  mapsncnv  6981  mptelixpg  7020  ixpsnf1o  7022  f1oen4g  7042  f1dom4g  7043  f1oen3g  7044  f1oeng  7047  en2d  7058  en3d  7059  dom2lem  7062  fundmen  7098  fundmeng  7099  unen  7109  modom  7112  rex2dom  7114  en2m  7117  xpdom2  7133  xpdom2g  7134  fopwdom  7140  nneneq  7162  phpm  7171  phpelm  7172  dif1enen  7188  fin0  7193  findcard  7196  diffifi  7202  ac6sfi  7206  onunsnss  7228  fiintim  7242  xpfi  7243  infidc  7252  fidcenum  7278  sbthlem1  7279  sbthlemi3  7281  sbthlemi10  7288  ffsuppbi  7305  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  fcdmnn0fsupp  9627  fcdmnn0suppg  9628  xnn0nnn0pnf  9654  elnnz  9665  zmulcl  9709  nn0n0n1ge2  9726  nn0lt2  9738  nn0le2is012  9739  uzind2  9769  nn0ind-raph  9774  eluzp1m1  9962  uz3m2nn  9989  supinfneg  10011  infsupneg  10012  infregelbex  10014  negm  10031  lbzbi  10032  qaddcl  10051  qmulcl  10053  qreccl  10058  elpq  10066  ledivge1le  10144  nn0ledivnn  10185  xrltne  10232  xrre  10239  xrre2  10240  xrre3  10241  ge0gtmnf  10242  xltnegi  10254  xnn0xadd0  10286  xnegdi  10287  xposdif  10301  xlesubadd  10302  iccsupr  10385  icoshft  10409  icoshftf1o  10410  fznlem  10462  fzen  10464  uzsubsubfz  10469  fzsuc2  10503  elfz1b  10514  elfz0ubfz0  10549  elfz0fzfz0  10550  fz0fzelfz0  10551  fz0fzdiffz0  10554  elfzmlbp  10556  difelfznle  10559  nn0p1elfzo  10611  fzofzim  10617  elincfzoext  10628  eluzgtdifelfzo  10632  elfzodifsumelfzo  10636  elfzonlteqm1  10645  elfzom1p1elfzo  10649  ssfzo12bi  10660  subfzo0  10678  zsupcllemex  10680  zssinfcl  10682  exbtwnzlemstep  10699  modqmuladdnn0  10826  modfzo0difsn  10853  addmodlteq  10856  frec2uzlt2d  10862  frecuzrdgtcl  10870  frecuzrdgfunlem  10877  seqf1og  10979  m1expcl2  11019  expge1  11034  leexp2r  11051  expubnd  11054  zesq  11117  expnlbnd  11123  nn0ltexp2  11169  nn0opthd  11182  faclbnd  11201  bcpasc  11226  hashprg  11271  hashf1  11309  seq3coll  11316  wrdnval  11357  wrdsymb0  11359  fstwrdne  11365  wrdred1hash  11370  swrdnd  11453  swrdwrdsymbg  11458  swrdsbslen  11460  swrdlsw  11463  swrdswrdlem  11498  swrdswrd  11499  pfxswrd  11500  cats1un  11515  wrd2ind  11517  swrdccatin1  11519  pfxccatin12lem4  11520  pfxccatin12lem2a  11521  pfxccatin12lem1  11522  swrdccatin2  11523  pfxccatin12lem2c  11524  pfxccatin12lem2  11525  pfxccatin12lem3  11526  pfxccatin12  11527  pfxccat3  11528  swrdccat  11529  pfxccat3a  11532  swrdccat3blem  11533  swrdccat3b  11534  swrdccatin2d  11538  reuccatpfxs1lem  11540  rexanuz  11776  rexuz3  11778  r19.29uz  11780  r19.2uz  11781  absnid  11861  leabs  11862  ltabs  11876  icodiamlt  11969  maxleast  12002  negfi  12017  climcn2  12100  climcau  12138  climcaucn  12142  sumdc  12149  fsum3cvg  12170  isumz  12181  fsumf1o  12182  fisumss  12184  isumss2  12185  fsumzcl2  12197  fsumsplit  12199  fsumsplitsnun  12211  sumsplitdc  12224  fsum2dlemstep  12226  telfsumo  12258  fsumparts  12262  fsumiun  12269  isumrpcl  12286  fproddccvg  12364  prod1dc  12378  prodssdc  12381  fprodssdc  12382  prodsnf  12384  fprodsplitdc  12388  fprod2dlemstep  12414  fprodmodd  12433  efexp  12474  efieq1re  12564  p1modz1  12586  dvds0lem  12593  dvds2ln  12616  dvdssub2  12627  dvdsadd2b  12632  dvdsabseq  12639  divconjdvds  12641  dvdsdivcl  12642  odd2np1  12665  oddge22np1  12673  opoe  12687  omoe  12688  opeo  12689  omeo  12690  m1expo  12692  nn0ehalf  12695  nn0o1gt2  12697  nno  12698  divalgb  12717  ndvdsadd  12723  bitsinv1lem  12753  gcd0id  12781  gcdneg  12784  gcdaddm  12786  bezoutlemstep  12799  dfgcd2  12816  gcddiv  12821  dvdsmulgcd  12827  bezoutr  12834  bezoutr1  12835  uzwodc  12839  nninfctlemfo  12842  algfx  12855  lcmgcdlem  12880  lcmgcdeq  12886  coprmdvds  12895  divgcdcoprmex  12905  cncongr1  12906  cncongr2  12907  isprm3  12921  dvdsnprmd  12928  prmgt1  12936  oddprmgt2  12938  isprm6  12951  cncongrprm  12961  phibndlem  13023  phimullem  13032  powm2modprm  13060  modprm0  13062  modprmn0modprm0  13064  prm23lt5  13071  pcneg  13133  pcprmpw2  13141  dvdsprmpweqnn  13144  dvdsprmpweqle  13145  pcaddlem  13147  fldivp1  13156  pcfac  13158  oddprmdvds  13162  prmunb  13170  ballotfilemfc0  13290  ballotfilemfcc  13291  ballotfilem4  13299  ballotfilemi1  13303  ballotfilemii  13304  ballotfilemic  13308  ballotfilem1c  13309  ballotfilemirc  13333  ballotfilem7  13337  ennnfone  13374  unct  13391  lidrididd  13761  sgrpass  13782  issgrpd  13786  issubmnd  13814  imasmnd2  13818  mnd1id  13822  insubm  13851  dfgrp2  13891  grpid  13903  grpasscan1  13927  dfgrp3mlem  13962  dfgrp3me  13964  imasgrp2  13972  mulgnn0gzsum  13990  mulgnn0p1  13995  mulgaddcom  14008  mulginvcom  14009  mulgass  14021  mulgpropdg  14026  subginv  14043  issubg2m  14051  issubg4m  14055  grpissubg  14056  resgrpisgrp  14057  subgintm  14060  kerf1ghm  14136  cmncom  14195  imasabl  14230  gsumvalfi  14242  rngdi  14346  rngdir  14347  rngpropd  14361  imasrng  14362  rng1zrlem  14365  imasring  14478  nzrunit  14604  issubrng2  14627  subrngintm  14629  issubrg2  14658  subrgintm  14660  lmodfopnelem1  14770  lmodfopnelem2  14771  lmodfopne  14772  islssm  14803  islidlm  14925  rnglidlmcl  14926  dflidl2rng  14927  rnglidlmmgm  14942  rnglidlmsgrp  14943  rnglidlrng  14944  gsumfsum  15032  dvdsrzring  15047  znidom  15101  issubassa3  15121  assamulgscmlem2  15151  uniopn  15227  istopon  15239  fiinbas  15275  tg2  15286  tgcl  15290  0nnei  15379  tgrest  15395  tgcn  15434  cnpnei  15445  cncnp2m  15457  lmtopcnp  15476  tx2cn  15496  txcn  15501  cnmpt21  15517  isxmet2d  15574  metrest  15732  metcnpi3  15743  tgioo  15780  fsumcncntop  15793  elcncf1di  15805  climcncf  15810  cncfco  15817  suplociccreex  15850  cnplimcim  15893  cnlimci  15899  reeff1olem  15997  efltlemlt  16000  efap1p  16005  sineq0re  16076  pellexlem1  16229  chtqub  16296  bpos1  16310  bposlem6  16316  zabsle1  16323  lgslem3  16326  lgsmod  16350  lgsdir2lem5  16356  lgsdir2  16357  lgsne0  16362  lgsdirnn0  16371  gausslemma2dlem0f  16378  gausslemma2dlem1a  16382  gausslemma2dlem3  16387  2lgslem1c  16414  2lgslem3a1  16421  2lgslem3b1  16422  2lgslem3c1  16423  2lgslem3d1  16424  2lgslem3  16425  2lgsoddprmlem2  16430  uhgrm  16524  incistruhgr  16536  upgrfnen  16544  umgrfnen  16554  umgrnloop  16562  upgredgpr  16595  usgrausgrben  16618  usgredgop  16619  usgruspgrben  16632  usgrislfuspgrdom  16636  umgrvad2edg  16657  ushgredgedg  16672  ushgredgedgloop  16674  uhgr0v0e  16680  subgreldmiedg  16715  subupgr  16719  uhgrspansubgrlem  16722  vtxdg0v  16740  wlkpropg  16770  wlkvg  16774  wlkl1loop  16804  upgriswlkdc  16806  upgrwlkedg  16807  upgrwlkvtxedg  16810  uspgr2wlkeq  16811  wlkres  16825  trlf1  16834  clwwlk1loop  16845  clwwlkccatlem  16846  isclwwlknx  16862  clwwlkn1loopb  16866  clwwlkext2edg  16868  umgr2cwwk2dif  16870  clwwlknonex2lem2  16884  clwwlknonex2  16885  eupthseg  16898  eupth2lem3lem4fi  16919  bj-charfun  17038  bj-charfunr  17041  bj-charfunbi  17042  bj-prexg  17142  peano5set  17171  bj-peano4  17186  bj-nn0suc  17195  bj-nn0sucALT  17209  bj-findis  17210  exmidsbthrlem  17273  trilpolemres  17298  trirec0  17300  nconstwlpolem  17322  neapmkv  17325  alsex  17346  ralsex  17347  als-no-surprise  17354