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  8501  cnegexlem2  8502  negf1o  8709  addgt0  8776  addgegt0  8777  addgtge0  8778  addge0  8779  recexre  8906  mulge0  8947  recexap  8981  prodgt02  9183  prodge02  9185  ltmul12a  9190  mulgt1  9193  nndivtr  9346  addltmul  9542  elnnnn0b  9607  fcdmnn0supp  9615  fcdmnn0fsupp  9616  fcdmnn0suppg  9617  xnn0nnn0pnf  9643  elnnz  9654  zmulcl  9698  nn0n0n1ge2  9715  nn0lt2  9727  nn0le2is012  9728  uzind2  9758  nn0ind-raph  9763  eluzp1m1  9946  uz3m2nn  9973  supinfneg  9995  infsupneg  9996  infregelbex  9998  negm  10015  lbzbi  10016  qaddcl  10035  qmulcl  10037  qreccl  10042  elpq  10049  ledivge1le  10127  nn0ledivnn  10168  xrltne  10215  xrre  10222  xrre2  10223  xrre3  10224  ge0gtmnf  10225  xltnegi  10237  xnn0xadd0  10269  xnegdi  10270  xposdif  10284  xlesubadd  10285  iccsupr  10368  icoshft  10392  icoshftf1o  10393  fznlem  10445  fzen  10447  uzsubsubfz  10452  fzsuc2  10486  elfz1b  10497  elfz0ubfz0  10532  elfz0fzfz0  10533  fz0fzelfz0  10534  fz0fzdiffz0  10537  elfzmlbp  10539  difelfznle  10542  nn0p1elfzo  10594  fzofzim  10600  elincfzoext  10611  eluzgtdifelfzo  10615  elfzodifsumelfzo  10619  elfzonlteqm1  10628  elfzom1p1elfzo  10632  ssfzo12bi  10643  subfzo0  10661  zsupcllemex  10663  zssinfcl  10665  exbtwnzlemstep  10682  modqmuladdnn0  10805  modfzo0difsn  10832  addmodlteq  10835  frec2uzlt2d  10841  frecuzrdgtcl  10849  frecuzrdgfunlem  10856  seqf1og  10958  m1expcl2  10998  expge1  11013  leexp2r  11030  expubnd  11033  zesq  11096  expnlbnd  11102  nn0ltexp2  11147  nn0opthd  11160  faclbnd  11179  bcpasc  11204  hashprg  11249  hashf1  11287  seq3coll  11294  wrdnval  11335  wrdsymb0  11337  fstwrdne  11343  wrdred1hash  11348  swrdnd  11431  swrdwrdsymbg  11436  swrdsbslen  11438  swrdlsw  11441  swrdswrdlem  11476  swrdswrd  11477  pfxswrd  11478  cats1un  11493  wrd2ind  11495  swrdccatin1  11497  pfxccatin12lem4  11498  pfxccatin12lem2a  11499  pfxccatin12lem1  11500  swrdccatin2  11501  pfxccatin12lem2c  11502  pfxccatin12lem2  11503  pfxccatin12lem3  11504  pfxccatin12  11505  pfxccat3  11506  swrdccat  11507  pfxccat3a  11510  swrdccat3blem  11511  swrdccat3b  11512  swrdccatin2d  11516  reuccatpfxs1lem  11518  rexanuz  11754  rexuz3  11756  r19.29uz  11758  r19.2uz  11759  absnid  11839  leabs  11840  ltabs  11853  icodiamlt  11946  maxleast  11979  negfi  11994  climcn2  12075  climcau  12113  climcaucn  12117  sumdc  12124  fsum3cvg  12145  isumz  12156  fsumf1o  12157  fisumss  12159  isumss2  12160  fsumzcl2  12172  fsumsplit  12174  fsumsplitsnun  12186  sumsplitdc  12199  fsum2dlemstep  12201  telfsumo  12233  fsumparts  12237  fsumiun  12244  isumrpcl  12261  fproddccvg  12339  prod1dc  12353  prodssdc  12356  fprodssdc  12357  prodsnf  12359  fprodsplitdc  12363  fprod2dlemstep  12389  fprodmodd  12408  efexp  12449  efieq1re  12539  p1modz1  12561  dvds0lem  12568  dvds2ln  12591  dvdssub2  12602  dvdsadd2b  12607  dvdsabseq  12614  divconjdvds  12616  dvdsdivcl  12617  odd2np1  12640  oddge22np1  12648  opoe  12662  omoe  12663  opeo  12664  omeo  12665  m1expo  12667  nn0ehalf  12670  nn0o1gt2  12672  nno  12673  divalgb  12692  ndvdsadd  12698  bitsinv1lem  12728  gcd0id  12756  gcdneg  12759  gcdaddm  12761  bezoutlemstep  12774  dfgcd2  12791  gcddiv  12796  dvdsmulgcd  12802  bezoutr  12809  bezoutr1  12810  uzwodc  12814  nninfctlemfo  12817  algfx  12830  lcmgcdlem  12855  lcmgcdeq  12861  coprmdvds  12870  divgcdcoprmex  12880  cncongr1  12881  cncongr2  12882  isprm3  12896  dvdsnprmd  12903  prmgt1  12910  oddprmgt2  12912  isprm6  12925  cncongrprm  12935  phibndlem  12994  phimullem  13003  powm2modprm  13031  modprm0  13033  modprmn0modprm0  13035  prm23lt5  13042  pcneg  13104  pcprmpw2  13112  dvdsprmpweqnn  13115  dvdsprmpweqle  13116  pcaddlem  13118  fldivp1  13127  pcfac  13129  oddprmdvds  13133  prmunb  13141  ballotfilemfc0  13232  ballotfilemfcc  13233  ballotfilem4  13241  ballotfilemi1  13245  ballotfilemii  13246  ballotfilemic  13250  ballotfilem1c  13251  ballotfilemirc  13275  ballotfilem7  13279  ennnfone  13316  unct  13333  lidrididd  13702  sgrpass  13723  issgrpd  13727  issubmnd  13755  imasmnd2  13759  mnd1id  13763  insubm  13792  dfgrp2  13832  grpid  13844  grpasscan1  13868  dfgrp3mlem  13903  dfgrp3me  13905  imasgrp2  13913  mulgnn0gzsum  13931  mulgnn0p1  13936  mulgaddcom  13949  mulginvcom  13950  mulgass  13962  mulgpropdg  13967  subginv  13984  issubg2m  13992  issubg4m  13996  grpissubg  13997  resgrpisgrp  13998  subgintm  14001  kerf1ghm  14077  cmncom  14105  imasabl  14140  gsumvalfi  14152  rngdi  14239  rngdir  14240  rngpropd  14254  imasrng  14255  rng1zrlem  14258  imasring  14369  nzrunit  14495  issubrng2  14518  subrngintm  14520  issubrg2  14549  subrgintm  14551  lmodfopnelem1  14661  lmodfopnelem2  14662  lmodfopne  14663  islssm  14694  islidlm  14816  rnglidlmcl  14817  dflidl2rng  14818  rnglidlmmgm  14833  rnglidlmsgrp  14834  rnglidlrng  14835  gsumfsum  14923  dvdsrzring  14938  znidom  14992  issubassa3  15012  assamulgscmlem2  15042  uniopn  15102  istopon  15114  fiinbas  15150  tg2  15161  tgcl  15165  0nnei  15254  tgrest  15270  tgcn  15309  cnpnei  15320  cncnp2m  15332  lmtopcnp  15351  tx2cn  15371  txcn  15376  cnmpt21  15392  isxmet2d  15449  metrest  15607  metcnpi3  15618  tgioo  15655  fsumcncntop  15668  elcncf1di  15680  climcncf  15685  cncfco  15692  suplociccreex  15725  cnplimcim  15768  cnlimci  15774  reeff1olem  15872  efltlemlt  15875  pellexlem1  16091  zabsle1  16118  lgslem3  16121  lgsmod  16145  lgsdir2lem5  16151  lgsdir2  16152  lgsne0  16157  lgsdirnn0  16166  gausslemma2dlem0f  16173  gausslemma2dlem1a  16177  gausslemma2dlem3  16182  2lgslem1c  16209  2lgslem3a1  16216  2lgslem3b1  16217  2lgslem3c1  16218  2lgslem3d1  16219  2lgslem3  16220  2lgsoddprmlem2  16225  uhgrm  16319  incistruhgr  16331  upgrfnen  16339  umgrfnen  16349  umgrnloop  16357  upgredgpr  16390  usgrausgrben  16413  usgredgop  16414  usgruspgrben  16427  usgrislfuspgrdom  16431  umgrvad2edg  16452  ushgredgedg  16467  ushgredgedgloop  16469  uhgr0v0e  16475  subgreldmiedg  16510  subupgr  16514  uhgrspansubgrlem  16517  vtxdg0v  16535  wlkpropg  16565  wlkvg  16569  wlkl1loop  16599  upgriswlkdc  16601  upgrwlkedg  16602  upgrwlkvtxedg  16605  uspgr2wlkeq  16606  wlkres  16620  trlf1  16629  clwwlk1loop  16640  clwwlkccatlem  16641  isclwwlknx  16657  clwwlkn1loopb  16661  clwwlkext2edg  16663  umgr2cwwk2dif  16665  clwwlknonex2lem2  16679  clwwlknonex2  16680  eupthseg  16693  eupth2lem3lem4fi  16714  bj-charfun  16833  bj-charfunr  16836  bj-charfunbi  16837  bj-prexg  16937  peano5set  16966  bj-peano4  16981  bj-nn0suc  16990  bj-nn0sucALT  17004  bj-findis  17005  exmidsbthrlem  17067  trilpolemres  17091  trirec0  17093  nconstwlpolem  17115  neapmkv  17118  alsex  17139  ralsex  17140  als-no-surprise  17147