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  4149  nbrne2  4150  mpteq12f  4211  triun  4242  csbexga  4261  prcssprc  4274  iinexgm  4290  prexg  4349  copsex2t  4385  swopo  4451  poirr  4452  potr  4453  pofun  4457  issod  4464  ordelss  4524  trssord  4525  limelon  4544  trsuc  4567  eusvnfb  4600  rabxfrd  4615  regexmidlem1  4680  nordeq  4691  suc11g  4704  nnsuc  4763  brrelex12  4813  vtoclr  4823  optocl  4851  relop  4930  brcogw  4949  breldmg  4987  elreldm  5008  riinint  5043  xpexcnvm  5142  issref  5170  xpidtr  5178  trin2  5179  cnveqb  5243  funopg  5411  funssres  5420  fununi  5449  funimass2  5459  imain  5463  fnun  5489  fco  5552  opelf  5560  f0rn0  5587  f1oun  5659  fun11iun  5660  fv3  5718  ndmfvg  5726  fvelima  5754  fvopab3ig  5779  fvmptssdm  5790  fvmptf  5798  fvimacnv  5824  fmptco  5874  fcof  5894  funfvima2  5951  funfvima3  5952  f1veqaeq  5975  f1ocnvfvrneq  5988  fliftfun  6002  isotr  6022  isoini  6024  isopolem  6028  isosolem  6030  moriotass  6069  acexmidlem2  6082  suppssov1  6299  f1dmex  6345  elabreximd  6356  releldm2  6419  f1o2ndf1  6464  poxp  6468  fsuppeq  6487  suppssfvg  6503  tposf2  6539  iunon  6555  smoel2  6574  tfrlem9  6590  tfrexlem  6605  tfr1onlembxssdm  6614  tfr1onlemres  6620  tfrcllembxssdm  6627  tfrcllemres  6633  tfrcl  6635  tfri3  6638  frecabcl  6670  sucinc2  6719  nnacom  6757  nnmcom  6762  nnsucsssuc  6765  nnsucuniel  6768  nntri2or2  6771  nnaordi  6781  nnmordi  6789  nnaordex  6801  nnm00  6803  ectocld  6875  iinerm  6881  th3qlem2  6912  elpm2r  6940  mapsnd  6970  mapsncnv  6977  mptelixpg  7016  ixpsnf1o  7018  f1oen4g  7038  f1dom4g  7039  f1oen3g  7040  f1oeng  7043  en2d  7054  en3d  7055  dom2lem  7058  fundmen  7094  fundmeng  7095  unen  7105  modom  7108  rex2dom  7110  en2m  7113  xpdom2  7129  xpdom2g  7130  fopwdom  7136  nneneq  7158  phpm  7167  phpelm  7168  dif1enen  7184  fin0  7189  findcard  7192  diffifi  7198  ac6sfi  7202  onunsnss  7224  fiintim  7238  xpfi  7239  infidc  7248  fidcenum  7273  sbthlem1  7274  sbthlemi3  7276  sbthlemi10  7283  ffsuppbi  7300  elfir  7307  isotilem  7346  inflbti  7364  ordiso2  7375  eldju2ndl  7412  eldju2ndr  7413  updjudhf  7419  mkvprop  7498  carden2bex  7535  pm54.43  7536  exmidfodomrlemeldju  7551  exmidfodomrlemreseldju  7552  exmidfodomrlemim  7553  pw1m  7583  ltmpig  7706  enq0sym  7799  addnq0mo  7814  mulnq0mo  7815  prarloclem3step  7863  prarloclem3  7864  genpml  7884  genpmu  7885  genprndl  7888  genprndu  7889  genpdisj  7890  distrlem1prl  7949  distrlem1pru  7950  distrlem4prl  7951  distrlem4pru  7952  distrlem5prl  7953  distrlem5pru  7954  ltsopr  7963  ltaddpr  7964  addcanprleml  7981  addcanprlemu  7982  recexprlemm  7991  recexprlemlol  7993  recexprlemupu  7995  aptiprleml  8006  aptiprlemu  8007  caucvgprlemnkj  8033  caucvgprlemnbj  8034  addsrmo  8110  mulsrmo  8111  srpospr  8150  caucvgsr  8169  axprecex  8247  mpomulf  8316  mulgt0  8400  ltne  8410  cnegexlem1  8502  cnegexlem2  8503  negf1o  8710  addgt0  8777  addgegt0  8778  addgtge0  8779  addge0  8780  recexre  8908  mulge0  8949  recexap  8983  prodgt02  9185  prodge02  9187  ltmul12a  9192  mulgt1  9195  nndivtr  9348  addltmul  9546  elnnnn0b  9611  fcdmnn0supp  9619  fcdmnn0fsupp  9620  fcdmnn0suppg  9621  xnn0nnn0pnf  9647  elnnz  9658  zmulcl  9702  nn0n0n1ge2  9719  nn0lt2  9731  nn0le2is012  9732  uzind2  9762  nn0ind-raph  9767  eluzp1m1  9955  uz3m2nn  9982  supinfneg  10004  infsupneg  10005  infregelbex  10007  negm  10024  lbzbi  10025  qaddcl  10044  qmulcl  10046  qreccl  10051  elpq  10059  ledivge1le  10137  nn0ledivnn  10178  xrltne  10225  xrre  10232  xrre2  10233  xrre3  10234  ge0gtmnf  10235  xltnegi  10247  xnn0xadd0  10279  xnegdi  10280  xposdif  10294  xlesubadd  10295  iccsupr  10378  icoshft  10402  icoshftf1o  10403  fznlem  10455  fzen  10457  uzsubsubfz  10462  fzsuc2  10496  elfz1b  10507  elfz0ubfz0  10542  elfz0fzfz0  10543  fz0fzelfz0  10544  fz0fzdiffz0  10547  elfzmlbp  10549  difelfznle  10552  nn0p1elfzo  10604  fzofzim  10610  elincfzoext  10621  eluzgtdifelfzo  10625  elfzodifsumelfzo  10629  elfzonlteqm1  10638  elfzom1p1elfzo  10642  ssfzo12bi  10653  subfzo0  10671  zsupcllemex  10673  zssinfcl  10675  exbtwnzlemstep  10692  modqmuladdnn0  10818  modfzo0difsn  10845  addmodlteq  10848  frec2uzlt2d  10854  frecuzrdgtcl  10862  frecuzrdgfunlem  10869  seqf1og  10971  m1expcl2  11011  expge1  11026  leexp2r  11043  expubnd  11046  zesq  11109  expnlbnd  11115  nn0ltexp2  11161  nn0opthd  11174  faclbnd  11193  bcpasc  11218  hashprg  11263  hashf1  11301  seq3coll  11308  wrdnval  11349  wrdsymb0  11351  fstwrdne  11357  wrdred1hash  11362  swrdnd  11445  swrdwrdsymbg  11450  swrdsbslen  11452  swrdlsw  11455  swrdswrdlem  11490  swrdswrd  11491  pfxswrd  11492  cats1un  11507  wrd2ind  11509  swrdccatin1  11511  pfxccatin12lem4  11512  pfxccatin12lem2a  11513  pfxccatin12lem1  11514  swrdccatin2  11515  pfxccatin12lem2c  11516  pfxccatin12lem2  11517  pfxccatin12lem3  11518  pfxccatin12  11519  pfxccat3  11520  swrdccat  11521  pfxccat3a  11524  swrdccat3blem  11525  swrdccat3b  11526  swrdccatin2d  11530  reuccatpfxs1lem  11532  rexanuz  11768  rexuz3  11770  r19.29uz  11772  r19.2uz  11773  absnid  11853  leabs  11854  ltabs  11868  icodiamlt  11961  maxleast  11994  negfi  12009  climcn2  12091  climcau  12129  climcaucn  12133  sumdc  12140  fsum3cvg  12161  isumz  12172  fsumf1o  12173  fisumss  12175  isumss2  12176  fsumzcl2  12188  fsumsplit  12190  fsumsplitsnun  12202  sumsplitdc  12215  fsum2dlemstep  12217  telfsumo  12249  fsumparts  12253  fsumiun  12260  isumrpcl  12277  fproddccvg  12355  prod1dc  12369  prodssdc  12372  fprodssdc  12373  prodsnf  12375  fprodsplitdc  12379  fprod2dlemstep  12405  fprodmodd  12424  efexp  12465  efieq1re  12555  p1modz1  12577  dvds0lem  12584  dvds2ln  12607  dvdssub2  12618  dvdsadd2b  12623  dvdsabseq  12630  divconjdvds  12632  dvdsdivcl  12633  odd2np1  12656  oddge22np1  12664  opoe  12678  omoe  12679  opeo  12680  omeo  12681  m1expo  12683  nn0ehalf  12686  nn0o1gt2  12688  nno  12689  divalgb  12708  ndvdsadd  12714  bitsinv1lem  12744  gcd0id  12772  gcdneg  12775  gcdaddm  12777  bezoutlemstep  12790  dfgcd2  12807  gcddiv  12812  dvdsmulgcd  12818  bezoutr  12825  bezoutr1  12826  uzwodc  12830  nninfctlemfo  12833  algfx  12846  lcmgcdlem  12871  lcmgcdeq  12877  coprmdvds  12886  divgcdcoprmex  12896  cncongr1  12897  cncongr2  12898  isprm3  12912  dvdsnprmd  12919  prmgt1  12927  oddprmgt2  12929  isprm6  12942  cncongrprm  12952  phibndlem  13014  phimullem  13023  powm2modprm  13051  modprm0  13053  modprmn0modprm0  13055  prm23lt5  13062  pcneg  13124  pcprmpw2  13132  dvdsprmpweqnn  13135  dvdsprmpweqle  13136  pcaddlem  13138  fldivp1  13147  pcfac  13149  oddprmdvds  13153  prmunb  13161  ballotfilemfc0  13281  ballotfilemfcc  13282  ballotfilem4  13290  ballotfilemi1  13294  ballotfilemii  13295  ballotfilemic  13299  ballotfilem1c  13300  ballotfilemirc  13324  ballotfilem7  13328  ennnfone  13365  unct  13382  lidrididd  13751  sgrpass  13772  issgrpd  13776  issubmnd  13804  imasmnd2  13808  mnd1id  13812  insubm  13841  dfgrp2  13881  grpid  13893  grpasscan1  13917  dfgrp3mlem  13952  dfgrp3me  13954  imasgrp2  13962  mulgnn0gzsum  13980  mulgnn0p1  13985  mulgaddcom  13998  mulginvcom  13999  mulgass  14011  mulgpropdg  14016  subginv  14033  issubg2m  14041  issubg4m  14045  grpissubg  14046  resgrpisgrp  14047  subgintm  14050  kerf1ghm  14126  cmncom  14154  imasabl  14189  gsumvalfi  14201  rngdi  14288  rngdir  14289  rngpropd  14303  imasrng  14304  rng1zrlem  14307  imasring  14418  nzrunit  14544  issubrng2  14567  subrngintm  14569  issubrg2  14598  subrgintm  14600  lmodfopnelem1  14710  lmodfopnelem2  14711  lmodfopne  14712  islssm  14743  islidlm  14865  rnglidlmcl  14866  dflidl2rng  14867  rnglidlmmgm  14882  rnglidlmsgrp  14883  rnglidlrng  14884  gsumfsum  14972  dvdsrzring  14987  znidom  15041  issubassa3  15061  assamulgscmlem2  15091  uniopn  15151  istopon  15163  fiinbas  15199  tg2  15210  tgcl  15214  0nnei  15303  tgrest  15319  tgcn  15358  cnpnei  15369  cncnp2m  15381  lmtopcnp  15400  tx2cn  15420  txcn  15425  cnmpt21  15441  isxmet2d  15498  metrest  15656  metcnpi3  15667  tgioo  15704  fsumcncntop  15717  elcncf1di  15729  climcncf  15734  cncfco  15741  suplociccreex  15774  cnplimcim  15817  cnlimci  15823  reeff1olem  15921  efltlemlt  15924  efap1p  15929  pellexlem1  16148  bpos1  16208  zabsle1  16216  lgslem3  16219  lgsmod  16243  lgsdir2lem5  16249  lgsdir2  16250  lgsne0  16255  lgsdirnn0  16264  gausslemma2dlem0f  16271  gausslemma2dlem1a  16275  gausslemma2dlem3  16280  2lgslem1c  16307  2lgslem3a1  16314  2lgslem3b1  16315  2lgslem3c1  16316  2lgslem3d1  16317  2lgslem3  16318  2lgsoddprmlem2  16323  uhgrm  16417  incistruhgr  16429  upgrfnen  16437  umgrfnen  16447  umgrnloop  16455  upgredgpr  16488  usgrausgrben  16511  usgredgop  16512  usgruspgrben  16525  usgrislfuspgrdom  16529  umgrvad2edg  16550  ushgredgedg  16565  ushgredgedgloop  16567  uhgr0v0e  16573  subgreldmiedg  16608  subupgr  16612  uhgrspansubgrlem  16615  vtxdg0v  16633  wlkpropg  16663  wlkvg  16667  wlkl1loop  16697  upgriswlkdc  16699  upgrwlkedg  16700  upgrwlkvtxedg  16703  uspgr2wlkeq  16704  wlkres  16718  trlf1  16727  clwwlk1loop  16738  clwwlkccatlem  16739  isclwwlknx  16755  clwwlkn1loopb  16759  clwwlkext2edg  16761  umgr2cwwk2dif  16763  clwwlknonex2lem2  16777  clwwlknonex2  16778  eupthseg  16791  eupth2lem3lem4fi  16812  bj-charfun  16931  bj-charfunr  16934  bj-charfunbi  16935  bj-prexg  17035  peano5set  17064  bj-peano4  17079  bj-nn0suc  17088  bj-nn0sucALT  17102  bj-findis  17103  exmidsbthrlem  17165  trilpolemres  17189  trirec0  17191  nconstwlpolem  17213  neapmkv  17216  alsex  17237  ralsex  17238  als-no-surprise  17245