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  693  imnan  697  jaoian  803  jaodan  805  stdcndc  853  impidc  866  pm2.5gdc  874  con2bidc  883  pm5.18dc  891  dfandc  892  pm4.63dc  894  pm4.54dc  910  pm4.79dc  911  orcanai  936  annimdc  946  pm4.55dc  947  orandc  948  pm4.82  959  pm3.11dc  966  pm3.12dc  967  dn1dc  969  3jcad  1205  3expia  1232  3an1rs  1246  3imp1  1247  3imp2  1249  syl3anl2  1323  3jaoian  1342  3jaodan  1343  mp3anl1  1368  mp3anl2  1369  mp3anl3  1370  ecased  1386  xor3dc  1432  pm5.15dc  1434  xor2dc  1435  xornbidc  1436  xordc  1437  nbbndc  1439  biassdc  1440  bilukdc  1441  dfbi3dc  1442  pm5.24dc  1443  xordidc  1444  alanimi  1508  19.29  1669  equs4  1773  equsexd  1778  spimth  1784  equs5a  1843  ax11v2  1869  ax11b  1875  equs5or  1879  sb5rf  1901  equvin  1912  nfsb4t  2070  eu5  2130  mopick  2161  euexex  2168  2euswapdc  2174  exists2  2180  eqrdav  2233  dvelimdc  2407  nebidc  2494  pm13.18  2495  nelne1  2504  nelne2  2505  rspa  2592  ralrimdvv  2628  r19.21bi  2632  r19.26  2671  ralbi  2677  rexbi  2678  r19.29  2682  vtoclgft  2867  rspcva  2921  rspc2va  2937  elabgt  2960  eqeu  2989  mob2  2999  mob  3001  euind  3006  reu6  3008  reuind  3024  sbctt  3111  rspsbca  3129  sbcnestgf  3192  rspcsbela  3200  ssel2  3235  sselda  3240  sstr  3248  nssne1  3298  nssne2  3299  reuss2  3503  reupick  3507  reupick2  3509  reximdva0m  3526  ssn0  3553  disjel  3565  ssdisj  3567  absneu  3765  preqr1g  3872  prel12  3877  dfiun2g  4025  nbrne1  4130  nbrne2  4131  mpteq12f  4192  triun  4223  csbexga  4240  prcssprc  4253  iinexgm  4268  prexg  4327  copsex2t  4363  swopo  4429  poirr  4430  potr  4431  pofun  4435  issod  4442  ordelss  4502  trssord  4503  limelon  4522  trsuc  4545  eusvnfb  4577  rabxfrd  4592  regexmidlem1  4657  nordeq  4668  suc11g  4681  nnsuc  4740  brrelex12  4790  vtoclr  4800  optocl  4828  relop  4907  brcogw  4926  breldmg  4964  elreldm  4985  riinint  5020  xpexcnvm  5119  issref  5147  xpidtr  5155  trin2  5156  cnveqb  5220  funopg  5388  funssres  5397  fununi  5426  funimass2  5436  imain  5440  fnun  5466  fco  5529  opelf  5537  f0rn0  5564  f1oun  5636  fun11iun  5637  fv3  5695  ndmfvg  5703  fvelima  5730  fvopab3ig  5753  fvmptssdm  5764  fvmptf  5772  fvimacnv  5795  fmptco  5845  fcof  5865  funfvima2  5921  funfvima3  5922  f1veqaeq  5944  f1ocnvfvrneq  5957  fliftfun  5971  isotr  5991  isoini  5993  isopolem  5997  isosolem  5999  moriotass  6036  acexmidlem2  6049  suppssov1  6265  f1dmex  6311  releldm2  6381  f1o2ndf1  6426  poxp  6430  fsuppeq  6449  suppssfvg  6465  tposf2  6501  iunon  6517  smoel2  6536  tfrlem9  6552  tfrexlem  6567  tfr1onlembxssdm  6576  tfr1onlemres  6582  tfrcllembxssdm  6589  tfrcllemres  6595  tfrcl  6597  tfri3  6600  frecabcl  6632  sucinc2  6681  nnacom  6719  nnmcom  6724  nnsucsssuc  6727  nnsucuniel  6730  nntri2or2  6733  nnaordi  6743  nnmordi  6751  nnaordex  6763  nnm00  6765  ectocld  6837  iinerm  6843  th3qlem2  6874  elpm2r  6902  mapsnd  6925  mapsncnv  6932  mptelixpg  6971  ixpsnf1o  6973  f1oen4g  6993  f1dom4g  6994  f1oen3g  6995  f1oeng  6998  en2d  7009  en3d  7010  dom2lem  7013  fundmen  7049  fundmeng  7050  unen  7060  modom  7063  rex2dom  7065  en2m  7068  xpdom2  7084  xpdom2g  7085  fopwdom  7091  nneneq  7113  phpm  7122  phpelm  7123  dif1enen  7139  fin0  7144  findcard  7147  diffifi  7153  ac6sfi  7157  onunsnss  7179  fiintim  7193  xpfi  7194  infidc  7203  fidcenum  7228  sbthlem1  7229  sbthlemi3  7231  sbthlemi10  7238  ffsuppbi  7255  elfir  7262  isotilem  7299  inflbti  7317  ordiso2  7328  eldju2ndl  7365  eldju2ndr  7366  updjudhf  7372  mkvprop  7451  carden2bex  7488  pm54.43  7489  exmidfodomrlemeldju  7504  exmidfodomrlemreseldju  7505  exmidfodomrlemim  7506  pw1m  7536  ltmpig  7656  enq0sym  7749  addnq0mo  7764  mulnq0mo  7765  prarloclem3step  7813  prarloclem3  7814  genpml  7834  genpmu  7835  genprndl  7838  genprndu  7839  genpdisj  7840  distrlem1prl  7899  distrlem1pru  7900  distrlem4prl  7901  distrlem4pru  7902  distrlem5prl  7903  distrlem5pru  7904  ltsopr  7913  ltaddpr  7914  addcanprleml  7931  addcanprlemu  7932  recexprlemm  7941  recexprlemlol  7943  recexprlemupu  7945  aptiprleml  7956  aptiprlemu  7957  caucvgprlemnkj  7983  caucvgprlemnbj  7984  addsrmo  8060  mulsrmo  8061  srpospr  8100  caucvgsr  8119  axprecex  8197  mpomulf  8266  mulgt0  8350  ltne  8360  cnegexlem1  8450  cnegexlem2  8451  negf1o  8657  addgt0  8724  addgegt0  8725  addgtge0  8726  addge0  8727  recexre  8854  mulge0  8895  recexap  8929  prodgt02  9129  prodge02  9131  ltmul12a  9136  mulgt1  9139  nndivtr  9281  addltmul  9477  elnnnn0b  9542  fcdmnn0supp  9550  fcdmnn0fsupp  9551  fcdmnn0suppg  9552  xnn0nnn0pnf  9578  elnnz  9589  zmulcl  9633  nn0n0n1ge2  9650  nn0lt2  9662  nn0le2is012  9663  uzind2  9693  nn0ind-raph  9698  eluzp1m1  9881  uz3m2nn  9908  supinfneg  9930  infsupneg  9931  infregelbex  9933  negm  9950  lbzbi  9951  qaddcl  9970  qmulcl  9972  qreccl  9977  elpq  9984  ledivge1le  10062  nn0ledivnn  10103  xrltne  10149  xrre  10156  xrre2  10157  xrre3  10158  ge0gtmnf  10159  xltnegi  10171  xnn0xadd0  10203  xnegdi  10204  xposdif  10218  xlesubadd  10219  iccsupr  10302  icoshft  10326  icoshftf1o  10327  fznlem  10378  fzen  10380  uzsubsubfz  10384  fzsuc2  10417  elfz1b  10428  elfz0ubfz0  10463  elfz0fzfz0  10464  fz0fzelfz0  10465  fz0fzdiffz0  10468  elfzmlbp  10470  difelfznle  10473  nn0p1elfzo  10525  fzofzim  10531  elincfzoext  10542  eluzgtdifelfzo  10546  elfzodifsumelfzo  10550  elfzonlteqm1  10559  elfzom1p1elfzo  10563  ssfzo12bi  10574  subfzo0  10592  zsupcllemex  10594  zssinfcl  10596  exbtwnzlemstep  10611  modqmuladdnn0  10734  modfzo0difsn  10761  addmodlteq  10764  frec2uzlt2d  10770  frecuzrdgtcl  10778  frecuzrdgfunlem  10785  seqf1og  10887  m1expcl2  10927  expge1  10942  leexp2r  10959  expubnd  10962  zesq  11024  expnlbnd  11030  nn0ltexp2  11075  nn0opthd  11088  faclbnd  11107  bcpasc  11132  hashprg  11177  seq3coll  11218  wrdnval  11259  wrdsymb0  11261  fstwrdne  11267  wrdred1hash  11272  swrdnd  11355  swrdwrdsymbg  11360  swrdsbslen  11362  swrdlsw  11365  swrdswrdlem  11400  swrdswrd  11401  pfxswrd  11402  cats1un  11417  wrd2ind  11419  swrdccatin1  11421  pfxccatin12lem4  11422  pfxccatin12lem2a  11423  pfxccatin12lem1  11424  swrdccatin2  11425  pfxccatin12lem2c  11426  pfxccatin12lem2  11427  pfxccatin12lem3  11428  pfxccatin12  11429  pfxccat3  11430  swrdccat  11431  pfxccat3a  11434  swrdccat3blem  11435  swrdccat3b  11436  swrdccatin2d  11440  reuccatpfxs1lem  11442  rexanuz  11677  rexuz3  11679  r19.29uz  11681  r19.2uz  11682  absnid  11762  leabs  11763  ltabs  11776  icodiamlt  11869  maxleast  11902  negfi  11917  climcn2  11998  climcau  12036  climcaucn  12040  sumdc  12047  fsum3cvg  12068  isumz  12079  fsumf1o  12080  fisumss  12082  isumss2  12083  fsumzcl2  12095  fsumsplit  12097  fsumsplitsnun  12109  sumsplitdc  12122  fsum2dlemstep  12124  telfsumo  12156  fsumparts  12160  fsumiun  12167  isumrpcl  12184  fproddccvg  12262  prod1dc  12276  prodssdc  12279  fprodssdc  12280  prodsnf  12282  fprodsplitdc  12286  fprod2dlemstep  12312  fprodmodd  12331  efexp  12372  efieq1re  12462  p1modz1  12484  dvds0lem  12491  dvds2ln  12514  dvdssub2  12525  dvdsadd2b  12530  dvdsabseq  12537  divconjdvds  12539  dvdsdivcl  12540  odd2np1  12563  oddge22np1  12571  opoe  12585  omoe  12586  opeo  12587  omeo  12588  m1expo  12590  nn0ehalf  12593  nn0o1gt2  12595  nno  12596  divalgb  12615  ndvdsadd  12621  bitsinv1lem  12651  gcd0id  12679  gcdneg  12682  gcdaddm  12684  bezoutlemstep  12697  dfgcd2  12714  gcddiv  12719  dvdsmulgcd  12725  bezoutr  12732  bezoutr1  12733  uzwodc  12737  nninfctlemfo  12740  algfx  12753  lcmgcdlem  12778  lcmgcdeq  12784  coprmdvds  12793  divgcdcoprmex  12803  cncongr1  12804  cncongr2  12805  isprm3  12819  dvdsnprmd  12826  prmgt1  12833  oddprmgt2  12835  isprm6  12848  cncongrprm  12858  phibndlem  12917  phimullem  12926  powm2modprm  12954  modprm0  12956  modprmn0modprm0  12958  prm23lt5  12965  pcneg  13027  pcprmpw2  13035  dvdsprmpweqnn  13038  dvdsprmpweqle  13039  pcaddlem  13041  fldivp1  13050  pcfac  13052  oddprmdvds  13056  prmunb  13064  ballotfilemfc0  13153  ballotfilemfcc  13154  ballotfilem4  13159  ennnfone  13193  unct  13210  lidrididd  13612  gsummgmpropd  13624  sgrpass  13638  issgrpd  13642  issubmnd  13672  imasmnd2  13682  mnd1id  13686  insubm  13715  dfgrp2  13757  grpid  13769  grpasscan1  13793  dfgrp3mlem  13828  dfgrp3me  13830  imasgrp2  13844  mulgnn0gsum  13862  mulgnn0p1  13867  mulgaddcom  13880  mulginvcom  13881  mulgass  13893  mulgpropdg  13898  subginv  13915  issubg2m  13923  issubg4m  13927  grpissubg  13928  resgrpisgrp  13929  subgintm  13932  kerf1ghm  14008  cmncom  14036  imasabl  14070  rngdi  14101  rngdir  14102  rngpropd  14116  imasrng  14117  imasring  14225  nzrunit  14350  issubrng2  14372  subrngintm  14374  issubrg2  14403  subrgintm  14405  lmodfopnelem1  14489  lmodfopnelem2  14490  lmodfopne  14491  islssm  14522  islidlm  14644  rnglidlmcl  14645  dflidl2rng  14646  rnglidlmmgm  14661  rnglidlmsgrp  14662  rnglidlrng  14663  dvdsrzring  14768  znidom  14822  uniopn  14883  istopon  14895  fiinbas  14931  tg2  14942  tgcl  14946  0nnei  15035  tgrest  15051  tgcn  15090  cnpnei  15101  cncnp2m  15113  lmtopcnp  15132  tx2cn  15152  txcn  15157  cnmpt21  15173  isxmet2d  15230  metrest  15388  metcnpi3  15399  tgioo  15436  fsumcncntop  15449  elcncf1di  15461  climcncf  15466  cncfco  15473  suplociccreex  15506  cnplimcim  15549  cnlimci  15555  reeff1olem  15653  efltlemlt  15656  pellexlem1  15862  zabsle1  15889  lgslem3  15892  lgsmod  15916  lgsdir2lem5  15922  lgsdir2  15923  lgsne0  15928  lgsdirnn0  15937  gausslemma2dlem0f  15944  gausslemma2dlem1a  15948  gausslemma2dlem3  15953  2lgslem1c  15980  2lgslem3a1  15987  2lgslem3b1  15988  2lgslem3c1  15989  2lgslem3d1  15990  2lgslem3  15991  2lgsoddprmlem2  15996  uhgrm  16090  incistruhgr  16102  upgrfnen  16110  umgrfnen  16120  umgrnloop  16128  upgredgpr  16161  usgrausgrben  16184  usgredgop  16185  usgruspgrben  16198  usgrislfuspgrdom  16202  umgrvad2edg  16223  ushgredgedg  16238  ushgredgedgloop  16240  uhgr0v0e  16246  subgreldmiedg  16281  subupgr  16285  uhgrspansubgrlem  16288  vtxdg0v  16306  wlkpropg  16336  wlkvg  16340  wlkl1loop  16370  upgriswlkdc  16372  upgrwlkedg  16373  upgrwlkvtxedg  16376  uspgr2wlkeq  16377  wlkres  16391  trlf1  16400  clwwlk1loop  16411  clwwlkccatlem  16412  isclwwlknx  16428  clwwlkn1loopb  16432  clwwlkext2edg  16434  umgr2cwwk2dif  16436  clwwlknonex2lem2  16450  clwwlknonex2  16451  eupthseg  16464  eupth2lem3lem4fi  16485  bj-charfun  16594  bj-charfunr  16597  bj-charfunbi  16598  bj-prexg  16698  peano5set  16727  bj-peano4  16742  bj-nn0suc  16751  bj-nn0sucALT  16765  bj-findis  16766  exmidsbthrlem  16819  trilpolemres  16843  trirec0  16845  nconstwlpolem  16868  neapmkv  16871  gfsumval  16879