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  558  anabsi5  579  anim12dan  600  pm3.43  602  con3dimp  636  annimim  687  imnan  691  jaoian  796  jaodan  798  stdcndc  846  impidc  859  pm2.5gdc  867  con2bidc  876  pm5.18dc  884  dfandc  885  pm4.63dc  887  pm4.54dc  903  pm4.79dc  904  orcanai  929  annimdc  939  pm4.55dc  940  orandc  941  pm4.82  952  pm3.11dc  959  pm3.12dc  960  dn1dc  962  3jcad  1180  3expia  1207  3an1rs  1221  3imp1  1222  3imp2  1224  syl3anl2  1298  3jaoian  1316  3jaodan  1317  mp3anl1  1342  mp3anl2  1343  mp3anl3  1344  ecased  1360  xor3dc  1398  pm5.15dc  1400  xor2dc  1401  xornbidc  1402  xordc  1403  nbbndc  1405  biassdc  1406  bilukdc  1407  dfbi3dc  1408  pm5.24dc  1409  xordidc  1410  alanimi  1470  19.29  1631  equs4  1736  equsexd  1740  spimth  1746  equs5a  1805  ax11v2  1831  ax11b  1837  equs5or  1841  sb5rf  1863  equvin  1874  nfsb4t  2030  eu5  2089  mopick  2120  euexex  2127  2euswapdc  2133  exists2  2139  eqrdav  2192  dvelimdc  2357  nebidc  2444  pm13.18  2445  nelne1  2454  nelne2  2455  rspa  2542  ralrimdvv  2578  r19.21bi  2582  r19.26  2620  ralbi  2626  rexbi  2627  r19.29  2631  vtoclgft  2811  rspcva  2863  rspc2va  2879  elabgt  2902  eqeu  2931  mob2  2941  mob  2943  euind  2948  reu6  2950  reuind  2966  sbctt  3053  rspsbca  3070  sbcnestgf  3133  rspcsbela  3141  ssel2  3175  sselda  3180  sstr  3188  nssne1  3238  nssne2  3239  reuss2  3440  reupick  3444  reupick2  3446  reximdva0m  3463  ssn0  3490  disjel  3502  ssdisj  3504  absneu  3691  preqr1g  3793  prel12  3798  dfiun2g  3945  nbrne1  4049  nbrne2  4050  mpteq12f  4110  triun  4141  csbexga  4158  iinexgm  4184  prexg  4241  copsex2t  4275  swopo  4338  poirr  4339  potr  4340  pofun  4344  issod  4351  ordelss  4411  trssord  4412  limelon  4431  trsuc  4454  eusvnfb  4486  rabxfrd  4501  regexmidlem1  4566  nordeq  4577  suc11g  4590  nnsuc  4649  brrelex12  4698  vtoclr  4708  optocl  4736  relop  4813  brcogw  4832  breldmg  4869  elreldm  4889  riinint  4924  issref  5049  xpidtr  5057  trin2  5058  cnveqb  5122  funopg  5289  funssres  5297  fununi  5323  funimass2  5333  imain  5337  fnun  5361  fco  5420  opelf  5426  f0rn0  5449  f1oun  5521  fun11iun  5522  fv3  5578  ndmfvg  5586  fvelima  5609  fvopab3ig  5632  fvmptssdm  5643  fvmptf  5651  fvimacnv  5674  fmptco  5725  funfvima2  5792  funfvima3  5793  f1veqaeq  5813  f1ocnvfvrneq  5826  fliftfun  5840  isotr  5860  isoini  5862  isopolem  5866  isosolem  5868  moriotass  5903  acexmidlem2  5916  suppssfv  6128  suppssov1  6129  f1dmex  6170  releldm2  6240  f1o2ndf1  6283  poxp  6287  tposf2  6323  iunon  6339  smoel2  6358  tfrlem9  6374  tfrexlem  6389  tfr1onlembxssdm  6398  tfr1onlemres  6404  tfrcllembxssdm  6411  tfrcllemres  6417  tfrcl  6419  tfri3  6422  frecabcl  6454  sucinc2  6501  nnacom  6539  nnmcom  6544  nnsucsssuc  6547  nnsucuniel  6550  nntri2or2  6553  nnaordi  6563  nnmordi  6571  nnaordex  6583  nnm00  6585  ectocld  6657  iinerm  6663  th3qlem2  6694  elpm2r  6722  mapsncnv  6751  mptelixpg  6790  ixpsnf1o  6792  f1oen3g  6810  f1oeng  6813  en2d  6824  en3d  6825  dom2lem  6828  fundmen  6862  fundmeng  6863  unen  6872  xpdom2  6887  xpdom2g  6888  fopwdom  6894  nneneq  6915  phpm  6923  phpelm  6924  dif1enen  6938  fin0  6943  findcard  6946  diffifi  6952  ac6sfi  6956  onunsnss  6975  fiintim  6987  xpfi  6988  infidc  6995  fidcenum  7017  sbthlem1  7018  sbthlemi3  7020  sbthlemi10  7027  elfir  7034  isotilem  7067  inflbti  7085  ordiso2  7096  eldju2ndl  7133  eldju2ndr  7134  updjudhf  7140  mkvprop  7219  carden2bex  7251  pm54.43  7252  exmidfodomrlemeldju  7261  exmidfodomrlemreseldju  7262  exmidfodomrlemim  7263  ltmpig  7401  enq0sym  7494  addnq0mo  7509  mulnq0mo  7510  prarloclem3step  7558  prarloclem3  7559  genpml  7579  genpmu  7580  genprndl  7583  genprndu  7584  genpdisj  7585  distrlem1prl  7644  distrlem1pru  7645  distrlem4prl  7646  distrlem4pru  7647  distrlem5prl  7648  distrlem5pru  7649  ltsopr  7658  ltaddpr  7659  addcanprleml  7676  addcanprlemu  7677  recexprlemm  7686  recexprlemlol  7688  recexprlemupu  7690  aptiprleml  7701  aptiprlemu  7702  caucvgprlemnkj  7728  caucvgprlemnbj  7729  addsrmo  7805  mulsrmo  7806  srpospr  7845  caucvgsr  7864  axprecex  7942  mpomulf  8011  mulgt0  8096  ltne  8106  cnegexlem1  8196  cnegexlem2  8197  negf1o  8403  addgt0  8469  addgegt0  8470  addgtge0  8471  addge0  8472  recexre  8599  mulge0  8640  recexap  8674  prodgt02  8874  prodge02  8876  ltmul12a  8881  mulgt1  8884  nndivtr  9026  addltmul  9222  elnnnn0b  9287  xnn0nnn0pnf  9319  elnnz  9330  zmulcl  9373  nn0n0n1ge2  9390  nn0lt2  9401  nn0le2is012  9402  uzind2  9432  nn0ind-raph  9437  eluzp1m1  9619  uz3m2nn  9641  supinfneg  9663  infsupneg  9664  infregelbex  9666  negm  9683  lbzbi  9684  qaddcl  9703  qmulcl  9705  qreccl  9710  elpq  9717  ledivge1le  9795  nn0ledivnn  9836  xrltne  9882  xrre  9889  xrre2  9890  xrre3  9891  ge0gtmnf  9892  xltnegi  9904  xnn0xadd0  9936  xnegdi  9937  xposdif  9951  xlesubadd  9952  iccsupr  10035  icoshft  10059  icoshftf1o  10060  fznlem  10110  fzen  10112  uzsubsubfz  10116  fzsuc2  10148  elfz1b  10159  elfz0ubfz0  10194  elfz0fzfz0  10195  fz0fzelfz0  10196  fz0fzdiffz0  10199  elfzmlbp  10201  difelfznle  10204  fzofzim  10258  eluzgtdifelfzo  10267  elfzodifsumelfzo  10271  elfzonlteqm1  10280  elfzom1p1elfzo  10284  ssfzo12bi  10295  subfzo0  10312  exbtwnzlemstep  10319  modqmuladdnn0  10442  modfzo0difsn  10469  addmodlteq  10472  frec2uzlt2d  10478  frecuzrdgtcl  10486  frecuzrdgfunlem  10493  seqf1og  10595  m1expcl2  10635  expge1  10650  leexp2r  10667  expubnd  10670  zesq  10732  expnlbnd  10738  nn0ltexp2  10783  nn0opthd  10796  faclbnd  10815  bcpasc  10840  hashprg  10882  seq3coll  10916  wrdnval  10947  wrdsymb0  10949  fstwrdne  10955  wrdred1hash  10960  rexanuz  11135  rexuz3  11137  r19.29uz  11139  r19.2uz  11140  absnid  11220  leabs  11221  ltabs  11234  icodiamlt  11327  maxleast  11360  negfi  11374  climcn2  11455  climcau  11493  climcaucn  11497  sumdc  11504  fsum3cvg  11524  isumz  11535  fsumf1o  11536  fisumss  11538  isumss2  11539  fsumzcl2  11551  fsumsplit  11553  fsumsplitsnun  11565  sumsplitdc  11578  fsum2dlemstep  11580  telfsumo  11612  fsumparts  11616  fsumiun  11623  isumrpcl  11640  fproddccvg  11718  prod1dc  11732  prodssdc  11735  fprodssdc  11736  prodsnf  11738  fprodsplitdc  11742  fprod2dlemstep  11768  fprodmodd  11787  efexp  11828  efieq1re  11918  p1modz1  11940  dvds0lem  11947  dvds2ln  11970  dvdssub2  11981  dvdsadd2b  11986  dvdsabseq  11992  divconjdvds  11994  dvdsdivcl  11995  odd2np1  12017  oddge22np1  12025  opoe  12039  omoe  12040  opeo  12041  omeo  12042  m1expo  12044  nn0ehalf  12047  nn0o1gt2  12049  nno  12050  divalgb  12069  ndvdsadd  12075  zsupcllemex  12086  zssinfcl  12088  gcd0id  12119  gcdneg  12122  gcdaddm  12124  bezoutlemstep  12137  dfgcd2  12154  gcddiv  12159  dvdsmulgcd  12165  bezoutr  12172  bezoutr1  12173  uzwodc  12177  nninfctlemfo  12180  algfx  12193  lcmgcdlem  12218  lcmgcdeq  12224  coprmdvds  12233  divgcdcoprmex  12243  cncongr1  12244  cncongr2  12245  isprm3  12259  dvdsnprmd  12266  prmgt1  12273  oddprmgt2  12275  isprm6  12288  cncongrprm  12298  phibndlem  12357  phimullem  12366  powm2modprm  12393  modprm0  12395  modprmn0modprm0  12397  prm23lt5  12404  pcneg  12466  pcprmpw2  12474  dvdsprmpweqnn  12477  dvdsprmpweqle  12478  pcaddlem  12480  fldivp1  12489  pcfac  12491  oddprmdvds  12495  prmunb  12503  ennnfone  12585  unct  12602  lidrididd  12968  gsummgmpropd  12980  sgrpass  12994  issgrpd  12998  issubmnd  13026  mnd1id  13031  insubm  13060  dfgrp2  13102  grpid  13114  grpasscan1  13138  dfgrp3mlem  13173  dfgrp3me  13175  imasgrp2  13183  mulgnn0gsum  13201  mulgnn0p1  13206  mulgaddcom  13219  mulginvcom  13220  mulgass  13232  mulgpropdg  13237  subginv  13254  issubg2m  13262  issubg4m  13266  grpissubg  13267  resgrpisgrp  13268  subgintm  13271  kerf1ghm  13347  cmncom  13375  imasabl  13409  rngdi  13439  rngdir  13440  rngpropd  13454  imasrng  13455  imasring  13563  nzrunit  13687  issubrng2  13709  subrngintm  13711  issubrg2  13740  subrgintm  13742  lmodfopnelem1  13823  lmodfopnelem2  13824  lmodfopne  13825  islssm  13856  islidlm  13978  rnglidlmcl  13979  dflidl2rng  13980  rnglidlmmgm  13995  rnglidlmsgrp  13996  rnglidlrng  13997  dvdsrzring  14102  znidom  14156  uniopn  14180  istopon  14192  fiinbas  14228  tg2  14239  tgcl  14243  0nnei  14332  tgrest  14348  tgcn  14387  cnpnei  14398  cncnp2m  14410  lmtopcnp  14429  tx2cn  14449  txcn  14454  cnmpt21  14470  isxmet2d  14527  metrest  14685  metcnpi3  14696  tgioo  14733  fsumcncntop  14746  elcncf1di  14758  climcncf  14763  cncfco  14770  suplociccreex  14803  cnplimcim  14846  cnlimci  14852  reeff1olem  14947  efltlemlt  14950  zabsle1  15156  lgslem3  15159  lgsmod  15183  lgsdir2lem5  15189  lgsdir2  15190  lgsne0  15195  lgsdirnn0  15204  gausslemma2dlem0f  15211  gausslemma2dlem1a  15215  gausslemma2dlem3  15220  2lgslem1c  15247  2lgslem3a1  15254  2lgslem3b1  15255  2lgslem3c1  15256  2lgslem3d1  15257  2lgslem3  15258  2lgsoddprmlem2  15263  bj-charfun  15369  bj-charfunr  15372  bj-charfunbi  15373  bj-prexg  15473  peano5set  15502  bj-peano4  15517  bj-nn0suc  15526  bj-nn0sucALT  15540  bj-findis  15541  exmidsbthrlem  15582  trilpolemres  15602  trirec0  15604  nconstwlpolem  15625  neapmkv  15628