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  7347  inflbti  7365  ordiso2  7376  eldju2ndl  7413  eldju2ndr  7414  updjudhf  7420  mkvprop  7499  carden2bex  7536  pm54.43  7537  exmidfodomrlemeldju  7552  exmidfodomrlemreseldju  7553  exmidfodomrlemim  7554  pw1m  7584  ltmpig  7707  enq0sym  7800  addnq0mo  7815  mulnq0mo  7816  prarloclem3step  7864  prarloclem3  7865  genpml  7885  genpmu  7886  genprndl  7889  genprndu  7890  genpdisj  7891  distrlem1prl  7950  distrlem1pru  7951  distrlem4prl  7952  distrlem4pru  7953  distrlem5prl  7954  distrlem5pru  7955  ltsopr  7964  ltaddpr  7965  addcanprleml  7982  addcanprlemu  7983  recexprlemm  7992  recexprlemlol  7994  recexprlemupu  7996  aptiprleml  8007  aptiprlemu  8008  caucvgprlemnkj  8034  caucvgprlemnbj  8035  addsrmo  8111  mulsrmo  8112  srpospr  8151  caucvgsr  8170  axprecex  8248  mpomulf  8317  mulgt0  8401  ltne  8411  cnegexlem1  8503  cnegexlem2  8504  negf1o  8711  addgt0  8778  addgegt0  8779  addgtge0  8780  addge0  8781  recexre  8909  mulge0  8950  recexap  8984  prodgt02  9186  prodge02  9188  ltmul12a  9193  mulgt1  9196  nndivtr  9349  addltmul  9547  elnnnn0b  9612  fcdmnn0supp  9620  fcdmnn0fsupp  9621  fcdmnn0suppg  9622  xnn0nnn0pnf  9648  elnnz  9659  zmulcl  9703  nn0n0n1ge2  9720  nn0lt2  9732  nn0le2is012  9733  uzind2  9763  nn0ind-raph  9768  eluzp1m1  9956  uz3m2nn  9983  supinfneg  10005  infsupneg  10006  infregelbex  10008  negm  10025  lbzbi  10026  qaddcl  10045  qmulcl  10047  qreccl  10052  elpq  10060  ledivge1le  10138  nn0ledivnn  10179  xrltne  10226  xrre  10233  xrre2  10234  xrre3  10235  ge0gtmnf  10236  xltnegi  10248  xnn0xadd0  10280  xnegdi  10281  xposdif  10295  xlesubadd  10296  iccsupr  10379  icoshft  10403  icoshftf1o  10404  fznlem  10456  fzen  10458  uzsubsubfz  10463  fzsuc2  10497  elfz1b  10508  elfz0ubfz0  10543  elfz0fzfz0  10544  fz0fzelfz0  10545  fz0fzdiffz0  10548  elfzmlbp  10550  difelfznle  10553  nn0p1elfzo  10605  fzofzim  10611  elincfzoext  10622  eluzgtdifelfzo  10626  elfzodifsumelfzo  10630  elfzonlteqm1  10639  elfzom1p1elfzo  10643  ssfzo12bi  10654  subfzo0  10672  zsupcllemex  10674  zssinfcl  10676  exbtwnzlemstep  10693  modqmuladdnn0  10820  modfzo0difsn  10847  addmodlteq  10850  frec2uzlt2d  10856  frecuzrdgtcl  10864  frecuzrdgfunlem  10871  seqf1og  10973  m1expcl2  11013  expge1  11028  leexp2r  11045  expubnd  11048  zesq  11111  expnlbnd  11117  nn0ltexp2  11163  nn0opthd  11176  faclbnd  11195  bcpasc  11220  hashprg  11265  hashf1  11303  seq3coll  11310  wrdnval  11351  wrdsymb0  11353  fstwrdne  11359  wrdred1hash  11364  swrdnd  11447  swrdwrdsymbg  11452  swrdsbslen  11454  swrdlsw  11457  swrdswrdlem  11492  swrdswrd  11493  pfxswrd  11494  cats1un  11509  wrd2ind  11511  swrdccatin1  11513  pfxccatin12lem4  11514  pfxccatin12lem2a  11515  pfxccatin12lem1  11516  swrdccatin2  11517  pfxccatin12lem2c  11518  pfxccatin12lem2  11519  pfxccatin12lem3  11520  pfxccatin12  11521  pfxccat3  11522  swrdccat  11523  pfxccat3a  11526  swrdccat3blem  11527  swrdccat3b  11528  swrdccatin2d  11532  reuccatpfxs1lem  11534  rexanuz  11770  rexuz3  11772  r19.29uz  11774  r19.2uz  11775  absnid  11855  leabs  11856  ltabs  11870  icodiamlt  11963  maxleast  11996  negfi  12011  climcn2  12094  climcau  12132  climcaucn  12136  sumdc  12143  fsum3cvg  12164  isumz  12175  fsumf1o  12176  fisumss  12178  isumss2  12179  fsumzcl2  12191  fsumsplit  12193  fsumsplitsnun  12205  sumsplitdc  12218  fsum2dlemstep  12220  telfsumo  12252  fsumparts  12256  fsumiun  12263  isumrpcl  12280  fproddccvg  12358  prod1dc  12372  prodssdc  12375  fprodssdc  12376  prodsnf  12378  fprodsplitdc  12382  fprod2dlemstep  12408  fprodmodd  12427  efexp  12468  efieq1re  12558  p1modz1  12580  dvds0lem  12587  dvds2ln  12610  dvdssub2  12621  dvdsadd2b  12626  dvdsabseq  12633  divconjdvds  12635  dvdsdivcl  12636  odd2np1  12659  oddge22np1  12667  opoe  12681  omoe  12682  opeo  12683  omeo  12684  m1expo  12686  nn0ehalf  12689  nn0o1gt2  12691  nno  12692  divalgb  12711  ndvdsadd  12717  bitsinv1lem  12747  gcd0id  12775  gcdneg  12778  gcdaddm  12780  bezoutlemstep  12793  dfgcd2  12810  gcddiv  12815  dvdsmulgcd  12821  bezoutr  12828  bezoutr1  12829  uzwodc  12833  nninfctlemfo  12836  algfx  12849  lcmgcdlem  12874  lcmgcdeq  12880  coprmdvds  12889  divgcdcoprmex  12899  cncongr1  12900  cncongr2  12901  isprm3  12915  dvdsnprmd  12922  prmgt1  12930  oddprmgt2  12932  isprm6  12945  cncongrprm  12955  phibndlem  13017  phimullem  13026  powm2modprm  13054  modprm0  13056  modprmn0modprm0  13058  prm23lt5  13065  pcneg  13127  pcprmpw2  13135  dvdsprmpweqnn  13138  dvdsprmpweqle  13139  pcaddlem  13141  fldivp1  13150  pcfac  13152  oddprmdvds  13156  prmunb  13164  ballotfilemfc0  13284  ballotfilemfcc  13285  ballotfilem4  13293  ballotfilemi1  13297  ballotfilemii  13298  ballotfilemic  13302  ballotfilem1c  13303  ballotfilemirc  13327  ballotfilem7  13331  ennnfone  13368  unct  13385  lidrididd  13755  sgrpass  13776  issgrpd  13780  issubmnd  13808  imasmnd2  13812  mnd1id  13816  insubm  13845  dfgrp2  13885  grpid  13897  grpasscan1  13921  dfgrp3mlem  13956  dfgrp3me  13958  imasgrp2  13966  mulgnn0gzsum  13984  mulgnn0p1  13989  mulgaddcom  14002  mulginvcom  14003  mulgass  14015  mulgpropdg  14020  subginv  14037  issubg2m  14045  issubg4m  14049  grpissubg  14050  resgrpisgrp  14051  subgintm  14054  kerf1ghm  14130  cmncom  14189  imasabl  14224  gsumvalfi  14236  rngdi  14323  rngdir  14324  rngpropd  14338  imasrng  14339  rng1zrlem  14342  imasring  14453  nzrunit  14579  issubrng2  14602  subrngintm  14604  issubrg2  14633  subrgintm  14635  lmodfopnelem1  14745  lmodfopnelem2  14746  lmodfopne  14747  islssm  14778  islidlm  14900  rnglidlmcl  14901  dflidl2rng  14902  rnglidlmmgm  14917  rnglidlmsgrp  14918  rnglidlrng  14919  gsumfsum  15007  dvdsrzring  15022  znidom  15076  issubassa3  15096  assamulgscmlem2  15126  uniopn  15193  istopon  15205  fiinbas  15241  tg2  15252  tgcl  15256  0nnei  15345  tgrest  15361  tgcn  15400  cnpnei  15411  cncnp2m  15423  lmtopcnp  15442  tx2cn  15462  txcn  15467  cnmpt21  15483  isxmet2d  15540  metrest  15698  metcnpi3  15709  tgioo  15746  fsumcncntop  15759  elcncf1di  15771  climcncf  15776  cncfco  15783  suplociccreex  15816  cnplimcim  15859  cnlimci  15865  reeff1olem  15963  efltlemlt  15966  efap1p  15971  pellexlem1  16190  chtqub  16257  bpos1  16271  bposlem6  16277  zabsle1  16284  lgslem3  16287  lgsmod  16311  lgsdir2lem5  16317  lgsdir2  16318  lgsne0  16323  lgsdirnn0  16332  gausslemma2dlem0f  16339  gausslemma2dlem1a  16343  gausslemma2dlem3  16348  2lgslem1c  16375  2lgslem3a1  16382  2lgslem3b1  16383  2lgslem3c1  16384  2lgslem3d1  16385  2lgslem3  16386  2lgsoddprmlem2  16391  uhgrm  16485  incistruhgr  16497  upgrfnen  16505  umgrfnen  16515  umgrnloop  16523  upgredgpr  16556  usgrausgrben  16579  usgredgop  16580  usgruspgrben  16593  usgrislfuspgrdom  16597  umgrvad2edg  16618  ushgredgedg  16633  ushgredgedgloop  16635  uhgr0v0e  16641  subgreldmiedg  16676  subupgr  16680  uhgrspansubgrlem  16683  vtxdg0v  16701  wlkpropg  16731  wlkvg  16735  wlkl1loop  16765  upgriswlkdc  16767  upgrwlkedg  16768  upgrwlkvtxedg  16771  uspgr2wlkeq  16772  wlkres  16786  trlf1  16795  clwwlk1loop  16806  clwwlkccatlem  16807  isclwwlknx  16823  clwwlkn1loopb  16827  clwwlkext2edg  16829  umgr2cwwk2dif  16831  clwwlknonex2lem2  16845  clwwlknonex2  16846  eupthseg  16859  eupth2lem3lem4fi  16880  bj-charfun  16999  bj-charfunr  17002  bj-charfunbi  17003  bj-prexg  17103  peano5set  17132  bj-peano4  17147  bj-nn0suc  17156  bj-nn0sucALT  17170  bj-findis  17171  exmidsbthrlem  17233  trilpolemres  17258  trirec0  17260  nconstwlpolem  17282  neapmkv  17285  alsex  17306  ralsex  17307  als-no-surprise  17314