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  2938  elabgt  2961  eqeu  2990  mob2  3000  mob  3002  euind  3007  reu6  3009  reuind  3025  sbctt  3112  rspsbca  3130  sbcnestgf  3193  rspcsbela  3201  ssel2  3237  sselda  3242  sstr  3250  nssne1  3300  nssne2  3301  reuss2  3505  reupick  3509  reupick2  3511  reximdva0m  3528  ssn0  3555  disjel  3567  ssdisj  3569  ifeqeqxdc  3673  absneu  3768  preqr1g  3875  prel12  3880  dfiun2g  4028  nbrne1  4133  nbrne2  4134  mpteq12f  4195  triun  4226  csbexga  4243  prcssprc  4256  iinexgm  4271  prexg  4330  copsex2t  4366  swopo  4432  poirr  4433  potr  4434  pofun  4438  issod  4445  ordelss  4505  trssord  4506  limelon  4525  trsuc  4548  eusvnfb  4580  rabxfrd  4595  regexmidlem1  4660  nordeq  4671  suc11g  4684  nnsuc  4743  brrelex12  4793  vtoclr  4803  optocl  4831  relop  4910  brcogw  4929  breldmg  4967  elreldm  4988  riinint  5023  xpexcnvm  5122  issref  5150  xpidtr  5158  trin2  5159  cnveqb  5223  funopg  5391  funssres  5400  fununi  5429  funimass2  5439  imain  5443  fnun  5469  fco  5532  opelf  5540  f0rn0  5567  f1oun  5639  fun11iun  5640  fv3  5698  ndmfvg  5706  fvelima  5733  fvopab3ig  5756  fvmptssdm  5767  fvmptf  5775  fvimacnv  5798  fmptco  5848  fcof  5868  funfvima2  5924  funfvima3  5925  f1veqaeq  5948  f1ocnvfvrneq  5961  fliftfun  5975  isotr  5995  isoini  5997  isopolem  6001  isosolem  6003  moriotass  6042  acexmidlem2  6055  suppssov1  6272  f1dmex  6318  elabreximd  6329  releldm2  6392  f1o2ndf1  6437  poxp  6441  fsuppeq  6460  suppssfvg  6476  tposf2  6512  iunon  6528  smoel2  6547  tfrlem9  6563  tfrexlem  6578  tfr1onlembxssdm  6587  tfr1onlemres  6593  tfrcllembxssdm  6600  tfrcllemres  6606  tfrcl  6608  tfri3  6611  frecabcl  6643  sucinc2  6692  nnacom  6730  nnmcom  6735  nnsucsssuc  6738  nnsucuniel  6741  nntri2or2  6744  nnaordi  6754  nnmordi  6762  nnaordex  6774  nnm00  6776  ectocld  6848  iinerm  6854  th3qlem2  6885  elpm2r  6913  mapsnd  6936  mapsncnv  6943  mptelixpg  6982  ixpsnf1o  6984  f1oen4g  7004  f1dom4g  7005  f1oen3g  7006  f1oeng  7009  en2d  7020  en3d  7021  dom2lem  7024  fundmen  7060  fundmeng  7061  unen  7071  modom  7074  rex2dom  7076  en2m  7079  xpdom2  7095  xpdom2g  7096  fopwdom  7102  nneneq  7124  phpm  7133  phpelm  7134  dif1enen  7150  fin0  7155  findcard  7158  diffifi  7164  ac6sfi  7168  onunsnss  7190  fiintim  7204  xpfi  7205  infidc  7214  fidcenum  7239  sbthlem1  7240  sbthlemi3  7242  sbthlemi10  7249  ffsuppbi  7266  elfir  7273  isotilem  7310  inflbti  7328  ordiso2  7339  eldju2ndl  7376  eldju2ndr  7377  updjudhf  7383  mkvprop  7462  carden2bex  7499  pm54.43  7500  exmidfodomrlemeldju  7515  exmidfodomrlemreseldju  7516  exmidfodomrlemim  7517  pw1m  7547  ltmpig  7670  enq0sym  7763  addnq0mo  7778  mulnq0mo  7779  prarloclem3step  7827  prarloclem3  7828  genpml  7848  genpmu  7849  genprndl  7852  genprndu  7853  genpdisj  7854  distrlem1prl  7913  distrlem1pru  7914  distrlem4prl  7915  distrlem4pru  7916  distrlem5prl  7917  distrlem5pru  7918  ltsopr  7927  ltaddpr  7928  addcanprleml  7945  addcanprlemu  7946  recexprlemm  7955  recexprlemlol  7957  recexprlemupu  7959  aptiprleml  7970  aptiprlemu  7971  caucvgprlemnkj  7997  caucvgprlemnbj  7998  addsrmo  8074  mulsrmo  8075  srpospr  8114  caucvgsr  8133  axprecex  8211  mpomulf  8280  mulgt0  8364  ltne  8374  cnegexlem1  8464  cnegexlem2  8465  negf1o  8672  addgt0  8739  addgegt0  8740  addgtge0  8741  addge0  8742  recexre  8869  mulge0  8910  recexap  8944  prodgt02  9144  prodge02  9146  ltmul12a  9151  mulgt1  9154  nndivtr  9296  addltmul  9492  elnnnn0b  9557  fcdmnn0supp  9565  fcdmnn0fsupp  9566  fcdmnn0suppg  9567  xnn0nnn0pnf  9593  elnnz  9604  zmulcl  9648  nn0n0n1ge2  9665  nn0lt2  9677  nn0le2is012  9678  uzind2  9708  nn0ind-raph  9713  eluzp1m1  9896  uz3m2nn  9923  supinfneg  9945  infsupneg  9946  infregelbex  9948  negm  9965  lbzbi  9966  qaddcl  9985  qmulcl  9987  qreccl  9992  elpq  9999  ledivge1le  10077  nn0ledivnn  10118  xrltne  10165  xrre  10172  xrre2  10173  xrre3  10174  ge0gtmnf  10175  xltnegi  10187  xnn0xadd0  10219  xnegdi  10220  xposdif  10234  xlesubadd  10235  iccsupr  10318  icoshft  10342  icoshftf1o  10343  fznlem  10395  fzen  10397  uzsubsubfz  10401  fzsuc2  10435  elfz1b  10446  elfz0ubfz0  10481  elfz0fzfz0  10482  fz0fzelfz0  10483  fz0fzdiffz0  10486  elfzmlbp  10488  difelfznle  10491  nn0p1elfzo  10543  fzofzim  10549  elincfzoext  10560  eluzgtdifelfzo  10564  elfzodifsumelfzo  10568  elfzonlteqm1  10577  elfzom1p1elfzo  10581  ssfzo12bi  10592  subfzo0  10610  zsupcllemex  10612  zssinfcl  10614  exbtwnzlemstep  10631  modqmuladdnn0  10754  modfzo0difsn  10781  addmodlteq  10784  frec2uzlt2d  10790  frecuzrdgtcl  10798  frecuzrdgfunlem  10805  seqf1og  10907  m1expcl2  10947  expge1  10962  leexp2r  10979  expubnd  10982  zesq  11045  expnlbnd  11051  nn0ltexp2  11096  nn0opthd  11109  faclbnd  11128  bcpasc  11153  hashprg  11198  seq3coll  11239  wrdnval  11280  wrdsymb0  11282  fstwrdne  11288  wrdred1hash  11293  swrdnd  11376  swrdwrdsymbg  11381  swrdsbslen  11383  swrdlsw  11386  swrdswrdlem  11421  swrdswrd  11422  pfxswrd  11423  cats1un  11438  wrd2ind  11440  swrdccatin1  11442  pfxccatin12lem4  11443  pfxccatin12lem2a  11444  pfxccatin12lem1  11445  swrdccatin2  11446  pfxccatin12lem2c  11447  pfxccatin12lem2  11448  pfxccatin12lem3  11449  pfxccatin12  11450  pfxccat3  11451  swrdccat  11452  pfxccat3a  11455  swrdccat3blem  11456  swrdccat3b  11457  swrdccatin2d  11461  reuccatpfxs1lem  11463  rexanuz  11698  rexuz3  11700  r19.29uz  11702  r19.2uz  11703  absnid  11783  leabs  11784  ltabs  11797  icodiamlt  11890  maxleast  11923  negfi  11938  climcn2  12019  climcau  12057  climcaucn  12061  sumdc  12068  fsum3cvg  12089  isumz  12100  fsumf1o  12101  fisumss  12103  isumss2  12104  fsumzcl2  12116  fsumsplit  12118  fsumsplitsnun  12130  sumsplitdc  12143  fsum2dlemstep  12145  telfsumo  12177  fsumparts  12181  fsumiun  12188  isumrpcl  12205  fproddccvg  12283  prod1dc  12297  prodssdc  12300  fprodssdc  12301  prodsnf  12303  fprodsplitdc  12307  fprod2dlemstep  12333  fprodmodd  12352  efexp  12393  efieq1re  12483  p1modz1  12505  dvds0lem  12512  dvds2ln  12535  dvdssub2  12546  dvdsadd2b  12551  dvdsabseq  12558  divconjdvds  12560  dvdsdivcl  12561  odd2np1  12584  oddge22np1  12592  opoe  12606  omoe  12607  opeo  12608  omeo  12609  m1expo  12611  nn0ehalf  12614  nn0o1gt2  12616  nno  12617  divalgb  12636  ndvdsadd  12642  bitsinv1lem  12672  gcd0id  12700  gcdneg  12703  gcdaddm  12705  bezoutlemstep  12718  dfgcd2  12735  gcddiv  12740  dvdsmulgcd  12746  bezoutr  12753  bezoutr1  12754  uzwodc  12758  nninfctlemfo  12761  algfx  12774  lcmgcdlem  12799  lcmgcdeq  12805  coprmdvds  12814  divgcdcoprmex  12824  cncongr1  12825  cncongr2  12826  isprm3  12840  dvdsnprmd  12847  prmgt1  12854  oddprmgt2  12856  isprm6  12869  cncongrprm  12879  phibndlem  12938  phimullem  12947  powm2modprm  12975  modprm0  12977  modprmn0modprm0  12979  prm23lt5  12986  pcneg  13048  pcprmpw2  13056  dvdsprmpweqnn  13059  dvdsprmpweqle  13060  pcaddlem  13062  fldivp1  13071  pcfac  13073  oddprmdvds  13077  prmunb  13085  ballotfilemfc0  13176  ballotfilemfcc  13177  ballotfilem4  13185  ballotfilemi1  13189  ballotfilemii  13190  ballotfilemic  13194  ballotfilem1c  13195  ballotfilemirc  13219  ballotfilem7  13223  ennnfone  13260  unct  13277  lidrididd  13645  gsummgmpropd  13657  sgrpass  13671  issgrpd  13675  issubmnd  13703  imasmnd2  13707  mnd1id  13711  insubm  13740  dfgrp2  13782  grpid  13794  grpasscan1  13818  dfgrp3mlem  13853  dfgrp3me  13855  imasgrp2  13863  mulgnn0gsum  13881  mulgnn0p1  13886  mulgaddcom  13899  mulginvcom  13900  mulgass  13912  mulgpropdg  13917  subginv  13934  issubg2m  13942  issubg4m  13946  grpissubg  13947  resgrpisgrp  13948  subgintm  13951  kerf1ghm  14027  cmncom  14055  imasabl  14089  gfsumval  14102  rngdi  14179  rngdir  14180  rngpropd  14194  imasrng  14195  rng1zrlem  14198  imasring  14307  nzrunit  14433  issubrng2  14456  subrngintm  14458  issubrg2  14487  subrgintm  14489  lmodfopnelem1  14598  lmodfopnelem2  14599  lmodfopne  14600  islssm  14631  islidlm  14753  rnglidlmcl  14754  dflidl2rng  14755  rnglidlmmgm  14770  rnglidlmsgrp  14771  rnglidlrng  14772  dvdsrzring  14877  znidom  14931  uniopn  14992  istopon  15004  fiinbas  15040  tg2  15051  tgcl  15055  0nnei  15144  tgrest  15160  tgcn  15199  cnpnei  15210  cncnp2m  15222  lmtopcnp  15241  tx2cn  15261  txcn  15266  cnmpt21  15282  isxmet2d  15339  metrest  15497  metcnpi3  15508  tgioo  15545  fsumcncntop  15558  elcncf1di  15570  climcncf  15575  cncfco  15582  suplociccreex  15615  cnplimcim  15658  cnlimci  15664  reeff1olem  15762  efltlemlt  15765  pellexlem1  15971  zabsle1  15998  lgslem3  16001  lgsmod  16025  lgsdir2lem5  16031  lgsdir2  16032  lgsne0  16037  lgsdirnn0  16046  gausslemma2dlem0f  16053  gausslemma2dlem1a  16057  gausslemma2dlem3  16062  2lgslem1c  16089  2lgslem3a1  16096  2lgslem3b1  16097  2lgslem3c1  16098  2lgslem3d1  16099  2lgslem3  16100  2lgsoddprmlem2  16105  uhgrm  16199  incistruhgr  16211  upgrfnen  16219  umgrfnen  16229  umgrnloop  16237  upgredgpr  16270  usgrausgrben  16293  usgredgop  16294  usgruspgrben  16307  usgrislfuspgrdom  16311  umgrvad2edg  16332  ushgredgedg  16347  ushgredgedgloop  16349  uhgr0v0e  16355  subgreldmiedg  16390  subupgr  16394  uhgrspansubgrlem  16397  vtxdg0v  16415  wlkpropg  16445  wlkvg  16449  wlkl1loop  16479  upgriswlkdc  16481  upgrwlkedg  16482  upgrwlkvtxedg  16485  uspgr2wlkeq  16486  wlkres  16500  trlf1  16509  clwwlk1loop  16520  clwwlkccatlem  16521  isclwwlknx  16537  clwwlkn1loopb  16541  clwwlkext2edg  16543  umgr2cwwk2dif  16545  clwwlknonex2lem2  16559  clwwlknonex2  16560  eupthseg  16573  eupth2lem3lem4fi  16594  bj-charfun  16703  bj-charfunr  16706  bj-charfunbi  16707  bj-prexg  16807  peano5set  16836  bj-peano4  16851  bj-nn0suc  16860  bj-nn0sucALT  16874  bj-findis  16875  exmidsbthrlem  16928  trilpolemres  16952  trirec0  16954  nconstwlpolem  16977  neapmkv  16980