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  1777  spimth  1783  equs5a  1842  ax11v2  1868  ax11b  1874  equs5or  1878  sb5rf  1900  equvin  1911  nfsb4t  2067  eu5  2127  mopick  2158  euexex  2165  2euswapdc  2171  exists2  2177  eqrdav  2230  dvelimdc  2396  nebidc  2483  pm13.18  2484  nelne1  2493  nelne2  2494  rspa  2581  ralrimdvv  2617  r19.21bi  2621  r19.26  2660  ralbi  2666  rexbi  2667  r19.29  2671  vtoclgft  2855  rspcva  2909  rspc2va  2925  elabgt  2948  eqeu  2977  mob2  2987  mob  2989  euind  2994  reu6  2996  reuind  3012  sbctt  3099  rspsbca  3117  sbcnestgf  3180  rspcsbela  3188  ssel2  3223  sselda  3228  sstr  3236  nssne1  3286  nssne2  3287  reuss2  3489  reupick  3493  reupick2  3495  reximdva0m  3512  ssn0  3539  disjel  3551  ssdisj  3553  absneu  3747  preqr1g  3854  prel12  3859  dfiun2g  4007  nbrne1  4112  nbrne2  4113  mpteq12f  4174  triun  4205  csbexga  4222  prcssprc  4235  iinexgm  4249  prexg  4307  copsex2t  4343  swopo  4409  poirr  4410  potr  4411  pofun  4415  issod  4422  ordelss  4482  trssord  4483  limelon  4502  trsuc  4525  eusvnfb  4557  rabxfrd  4572  regexmidlem1  4637  nordeq  4648  suc11g  4661  nnsuc  4720  brrelex12  4770  vtoclr  4780  optocl  4808  relop  4886  brcogw  4905  breldmg  4943  elreldm  4964  riinint  4999  xpexcnvm  5098  issref  5126  xpidtr  5134  trin2  5135  cnveqb  5199  funopg  5367  funssres  5376  fununi  5405  funimass2  5415  imain  5419  fnun  5445  fco  5507  opelf  5515  f0rn0  5540  f1oun  5612  fun11iun  5613  fv3  5671  ndmfvg  5679  fvelima  5706  fvopab3ig  5729  fvmptssdm  5740  fvmptf  5748  fvimacnv  5771  fmptco  5821  fcof  5841  funfvima2  5897  funfvima3  5898  f1veqaeq  5920  f1ocnvfvrneq  5933  fliftfun  5947  isotr  5967  isoini  5969  isopolem  5973  isosolem  5975  moriotass  6012  acexmidlem2  6025  suppssov1  6241  f1dmex  6287  releldm2  6357  f1o2ndf1  6402  poxp  6406  fsuppeq  6425  suppssfvg  6441  tposf2  6477  iunon  6493  smoel2  6512  tfrlem9  6528  tfrexlem  6543  tfr1onlembxssdm  6552  tfr1onlemres  6558  tfrcllembxssdm  6565  tfrcllemres  6571  tfrcl  6573  tfri3  6576  frecabcl  6608  sucinc2  6657  nnacom  6695  nnmcom  6700  nnsucsssuc  6703  nnsucuniel  6706  nntri2or2  6709  nnaordi  6719  nnmordi  6727  nnaordex  6739  nnm00  6741  ectocld  6813  iinerm  6819  th3qlem2  6850  elpm2r  6878  mapsncnv  6907  mptelixpg  6946  ixpsnf1o  6948  f1oen4g  6968  f1dom4g  6969  f1oen3g  6970  f1oeng  6973  en2d  6984  en3d  6985  dom2lem  6988  fundmen  7024  fundmeng  7025  unen  7034  modom  7037  rex2dom  7039  en2m  7042  xpdom2  7058  xpdom2g  7059  fopwdom  7065  nneneq  7086  phpm  7095  phpelm  7096  dif1enen  7112  fin0  7117  findcard  7120  diffifi  7126  ac6sfi  7130  onunsnss  7152  fiintim  7166  xpfi  7167  infidc  7176  fidcenum  7198  sbthlem1  7199  sbthlemi3  7201  sbthlemi10  7208  ffsuppbi  7225  elfir  7232  isotilem  7265  inflbti  7283  ordiso2  7294  eldju2ndl  7331  eldju2ndr  7332  updjudhf  7338  mkvprop  7417  carden2bex  7454  pm54.43  7455  exmidfodomrlemeldju  7470  exmidfodomrlemreseldju  7471  exmidfodomrlemim  7472  pw1m  7502  ltmpig  7619  enq0sym  7712  addnq0mo  7727  mulnq0mo  7728  prarloclem3step  7776  prarloclem3  7777  genpml  7797  genpmu  7798  genprndl  7801  genprndu  7802  genpdisj  7803  distrlem1prl  7862  distrlem1pru  7863  distrlem4prl  7864  distrlem4pru  7865  distrlem5prl  7866  distrlem5pru  7867  ltsopr  7876  ltaddpr  7877  addcanprleml  7894  addcanprlemu  7895  recexprlemm  7904  recexprlemlol  7906  recexprlemupu  7908  aptiprleml  7919  aptiprlemu  7920  caucvgprlemnkj  7946  caucvgprlemnbj  7947  addsrmo  8023  mulsrmo  8024  srpospr  8063  caucvgsr  8082  axprecex  8160  mpomulf  8229  mulgt0  8313  ltne  8323  cnegexlem1  8413  cnegexlem2  8414  negf1o  8620  addgt0  8687  addgegt0  8688  addgtge0  8689  addge0  8690  recexre  8817  mulge0  8858  recexap  8892  prodgt02  9092  prodge02  9094  ltmul12a  9099  mulgt1  9102  nndivtr  9244  addltmul  9440  elnnnn0b  9505  fcdmnn0supp  9513  fcdmnn0suppg  9514  xnn0nnn0pnf  9539  elnnz  9550  zmulcl  9594  nn0n0n1ge2  9611  nn0lt2  9622  nn0le2is012  9623  uzind2  9653  nn0ind-raph  9658  eluzp1m1  9841  uz3m2nn  9868  supinfneg  9890  infsupneg  9891  infregelbex  9893  negm  9910  lbzbi  9911  qaddcl  9930  qmulcl  9932  qreccl  9937  elpq  9944  ledivge1le  10022  nn0ledivnn  10063  xrltne  10109  xrre  10116  xrre2  10117  xrre3  10118  ge0gtmnf  10119  xltnegi  10131  xnn0xadd0  10163  xnegdi  10164  xposdif  10178  xlesubadd  10179  iccsupr  10262  icoshft  10286  icoshftf1o  10287  fznlem  10338  fzen  10340  uzsubsubfz  10344  fzsuc2  10376  elfz1b  10387  elfz0ubfz0  10422  elfz0fzfz0  10423  fz0fzelfz0  10424  fz0fzdiffz0  10427  elfzmlbp  10429  difelfznle  10432  nn0p1elfzo  10484  fzofzim  10490  elincfzoext  10501  eluzgtdifelfzo  10505  elfzodifsumelfzo  10509  elfzonlteqm1  10518  elfzom1p1elfzo  10522  ssfzo12bi  10533  subfzo0  10551  zsupcllemex  10553  zssinfcl  10555  exbtwnzlemstep  10570  modqmuladdnn0  10693  modfzo0difsn  10720  addmodlteq  10723  frec2uzlt2d  10729  frecuzrdgtcl  10737  frecuzrdgfunlem  10744  seqf1og  10846  m1expcl2  10886  expge1  10901  leexp2r  10918  expubnd  10921  zesq  10983  expnlbnd  10989  nn0ltexp2  11034  nn0opthd  11047  faclbnd  11066  bcpasc  11091  hashprg  11135  seq3coll  11169  wrdnval  11210  wrdsymb0  11212  fstwrdne  11218  wrdred1hash  11223  swrdnd  11306  swrdwrdsymbg  11311  swrdsbslen  11313  swrdlsw  11316  swrdswrdlem  11351  swrdswrd  11352  pfxswrd  11353  cats1un  11368  wrd2ind  11370  swrdccatin1  11372  pfxccatin12lem4  11373  pfxccatin12lem2a  11374  pfxccatin12lem1  11375  swrdccatin2  11376  pfxccatin12lem2c  11377  pfxccatin12lem2  11378  pfxccatin12lem3  11379  pfxccatin12  11380  pfxccat3  11381  swrdccat  11382  pfxccat3a  11385  swrdccat3blem  11386  swrdccat3b  11387  swrdccatin2d  11391  reuccatpfxs1lem  11393  rexanuz  11628  rexuz3  11630  r19.29uz  11632  r19.2uz  11633  absnid  11713  leabs  11714  ltabs  11727  icodiamlt  11820  maxleast  11853  negfi  11868  climcn2  11949  climcau  11987  climcaucn  11991  sumdc  11998  fsum3cvg  12019  isumz  12030  fsumf1o  12031  fisumss  12033  isumss2  12034  fsumzcl2  12046  fsumsplit  12048  fsumsplitsnun  12060  sumsplitdc  12073  fsum2dlemstep  12075  telfsumo  12107  fsumparts  12111  fsumiun  12118  isumrpcl  12135  fproddccvg  12213  prod1dc  12227  prodssdc  12230  fprodssdc  12231  prodsnf  12233  fprodsplitdc  12237  fprod2dlemstep  12263  fprodmodd  12282  efexp  12323  efieq1re  12413  p1modz1  12435  dvds0lem  12442  dvds2ln  12465  dvdssub2  12476  dvdsadd2b  12481  dvdsabseq  12488  divconjdvds  12490  dvdsdivcl  12491  odd2np1  12514  oddge22np1  12522  opoe  12536  omoe  12537  opeo  12538  omeo  12539  m1expo  12541  nn0ehalf  12544  nn0o1gt2  12546  nno  12547  divalgb  12566  ndvdsadd  12572  bitsinv1lem  12602  gcd0id  12630  gcdneg  12633  gcdaddm  12635  bezoutlemstep  12648  dfgcd2  12665  gcddiv  12670  dvdsmulgcd  12676  bezoutr  12683  bezoutr1  12684  uzwodc  12688  nninfctlemfo  12691  algfx  12704  lcmgcdlem  12729  lcmgcdeq  12735  coprmdvds  12744  divgcdcoprmex  12754  cncongr1  12755  cncongr2  12756  isprm3  12770  dvdsnprmd  12777  prmgt1  12784  oddprmgt2  12786  isprm6  12799  cncongrprm  12809  phibndlem  12868  phimullem  12877  powm2modprm  12905  modprm0  12907  modprmn0modprm0  12909  prm23lt5  12916  pcneg  12978  pcprmpw2  12986  dvdsprmpweqnn  12989  dvdsprmpweqle  12990  pcaddlem  12992  fldivp1  13001  pcfac  13003  oddprmdvds  13007  prmunb  13015  ennnfone  13126  unct  13143  lidrididd  13545  gsummgmpropd  13557  sgrpass  13571  issgrpd  13575  issubmnd  13605  imasmnd2  13615  mnd1id  13619  insubm  13648  dfgrp2  13690  grpid  13702  grpasscan1  13726  dfgrp3mlem  13761  dfgrp3me  13763  imasgrp2  13777  mulgnn0gsum  13795  mulgnn0p1  13800  mulgaddcom  13813  mulginvcom  13814  mulgass  13826  mulgpropdg  13831  subginv  13848  issubg2m  13856  issubg4m  13860  grpissubg  13861  resgrpisgrp  13862  subgintm  13865  kerf1ghm  13941  cmncom  13969  imasabl  14003  rngdi  14034  rngdir  14035  rngpropd  14049  imasrng  14050  imasring  14158  nzrunit  14283  issubrng2  14305  subrngintm  14307  issubrg2  14336  subrgintm  14338  lmodfopnelem1  14420  lmodfopnelem2  14421  lmodfopne  14422  islssm  14453  islidlm  14575  rnglidlmcl  14576  dflidl2rng  14577  rnglidlmmgm  14592  rnglidlmsgrp  14593  rnglidlrng  14594  dvdsrzring  14699  znidom  14753  uniopn  14812  istopon  14824  fiinbas  14860  tg2  14871  tgcl  14875  0nnei  14964  tgrest  14980  tgcn  15019  cnpnei  15030  cncnp2m  15042  lmtopcnp  15061  tx2cn  15081  txcn  15086  cnmpt21  15102  isxmet2d  15159  metrest  15317  metcnpi3  15328  tgioo  15365  fsumcncntop  15378  elcncf1di  15390  climcncf  15395  cncfco  15402  suplociccreex  15435  cnplimcim  15478  cnlimci  15484  reeff1olem  15582  efltlemlt  15585  pellexlem1  15791  zabsle1  15818  lgslem3  15821  lgsmod  15845  lgsdir2lem5  15851  lgsdir2  15852  lgsne0  15857  lgsdirnn0  15866  gausslemma2dlem0f  15873  gausslemma2dlem1a  15877  gausslemma2dlem3  15882  2lgslem1c  15909  2lgslem3a1  15916  2lgslem3b1  15917  2lgslem3c1  15918  2lgslem3d1  15919  2lgslem3  15920  2lgsoddprmlem2  15925  uhgrm  16019  incistruhgr  16031  upgrfnen  16039  umgrfnen  16049  umgrnloop  16057  upgredgpr  16090  usgrausgrben  16113  usgredgop  16114  usgruspgrben  16127  usgrislfuspgrdom  16131  umgrvad2edg  16152  ushgredgedg  16167  ushgredgedgloop  16169  uhgr0v0e  16175  subgreldmiedg  16210  subupgr  16214  uhgrspansubgrlem  16217  vtxdg0v  16235  wlkpropg  16265  wlkvg  16269  wlkl1loop  16299  upgriswlkdc  16301  upgrwlkedg  16302  upgrwlkvtxedg  16305  uspgr2wlkeq  16306  wlkres  16320  trlf1  16329  clwwlk1loop  16340  clwwlkccatlem  16341  isclwwlknx  16357  clwwlkn1loopb  16361  clwwlkext2edg  16363  umgr2cwwk2dif  16365  clwwlknonex2lem2  16379  clwwlknonex2  16380  eupthseg  16393  eupth2lem3lem4fi  16414  bj-charfun  16523  bj-charfunr  16526  bj-charfunbi  16527  bj-prexg  16627  peano5set  16656  bj-peano4  16671  bj-nn0suc  16680  bj-nn0sucALT  16694  bj-findis  16695  exmidsbthrlem  16750  trilpolemres  16774  trirec0  16776  nconstwlpolem  16798  neapmkv  16801  gfsumval  16809