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  692  imnan  696  jaoian  802  jaodan  804  stdcndc  852  impidc  865  pm2.5gdc  873  con2bidc  882  pm5.18dc  890  dfandc  891  pm4.63dc  893  pm4.54dc  909  pm4.79dc  910  orcanai  935  annimdc  945  pm4.55dc  946  orandc  947  pm4.82  958  pm3.11dc  965  pm3.12dc  966  dn1dc  968  3jcad  1204  3expia  1231  3an1rs  1245  3imp1  1246  3imp2  1248  syl3anl2  1322  3jaoian  1341  3jaodan  1342  mp3anl1  1367  mp3anl2  1368  mp3anl3  1369  ecased  1385  xor3dc  1431  pm5.15dc  1433  xor2dc  1434  xornbidc  1435  xordc  1436  nbbndc  1438  biassdc  1439  bilukdc  1440  dfbi3dc  1441  pm5.24dc  1442  xordidc  1443  alanimi  1507  19.29  1668  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  2395  nebidc  2482  pm13.18  2483  nelne1  2492  nelne2  2493  rspa  2580  ralrimdvv  2616  r19.21bi  2620  r19.26  2659  ralbi  2665  rexbi  2666  r19.29  2670  vtoclgft  2854  rspcva  2908  rspc2va  2924  elabgt  2947  eqeu  2976  mob2  2986  mob  2988  euind  2993  reu6  2995  reuind  3011  sbctt  3098  rspsbca  3116  sbcnestgf  3179  rspcsbela  3187  ssel2  3222  sselda  3227  sstr  3235  nssne1  3285  nssne2  3286  reuss2  3487  reupick  3491  reupick2  3493  reximdva0m  3510  ssn0  3537  disjel  3549  ssdisj  3551  absneu  3743  preqr1g  3849  prel12  3854  dfiun2g  4002  nbrne1  4107  nbrne2  4108  mpteq12f  4169  triun  4200  csbexga  4217  prcssprc  4230  iinexgm  4244  prexg  4301  copsex2t  4337  swopo  4403  poirr  4404  potr  4405  pofun  4409  issod  4416  ordelss  4476  trssord  4477  limelon  4496  trsuc  4519  eusvnfb  4551  rabxfrd  4566  regexmidlem1  4631  nordeq  4642  suc11g  4655  nnsuc  4714  brrelex12  4764  vtoclr  4774  optocl  4802  relop  4880  brcogw  4899  breldmg  4937  elreldm  4958  riinint  4993  issref  5119  xpidtr  5127  trin2  5128  cnveqb  5192  funopg  5360  funssres  5369  fununi  5398  funimass2  5408  imain  5412  fnun  5438  fco  5500  opelf  5507  f0rn0  5531  f1oun  5603  fun11iun  5604  fv3  5662  ndmfvg  5670  fvelima  5697  fvopab3ig  5720  fvmptssdm  5731  fvmptf  5739  fvimacnv  5762  fmptco  5813  fcof  5832  funfvima2  5886  funfvima3  5887  f1veqaeq  5909  f1ocnvfvrneq  5922  fliftfun  5936  isotr  5956  isoini  5958  isopolem  5962  isosolem  5964  moriotass  6001  acexmidlem2  6014  suppssfv  6230  suppssov1  6231  f1dmex  6277  releldm2  6347  f1o2ndf1  6392  poxp  6396  tposf2  6433  iunon  6449  smoel2  6468  tfrlem9  6484  tfrexlem  6499  tfr1onlembxssdm  6508  tfr1onlemres  6514  tfrcllembxssdm  6521  tfrcllemres  6527  tfrcl  6529  tfri3  6532  frecabcl  6564  sucinc2  6613  nnacom  6651  nnmcom  6656  nnsucsssuc  6659  nnsucuniel  6662  nntri2or2  6665  nnaordi  6675  nnmordi  6683  nnaordex  6695  nnm00  6697  ectocld  6769  iinerm  6775  th3qlem2  6806  elpm2r  6834  mapsncnv  6863  mptelixpg  6902  ixpsnf1o  6904  f1oen4g  6924  f1dom4g  6925  f1oen3g  6926  f1oeng  6929  en2d  6940  en3d  6941  dom2lem  6944  fundmen  6980  fundmeng  6981  unen  6990  modom  6993  rex2dom  6995  en2m  6998  xpdom2  7014  xpdom2g  7015  fopwdom  7021  nneneq  7042  phpm  7051  phpelm  7052  dif1enen  7068  fin0  7073  findcard  7076  diffifi  7082  ac6sfi  7086  onunsnss  7108  fiintim  7122  xpfi  7123  infidc  7132  fidcenum  7154  sbthlem1  7155  sbthlemi3  7157  sbthlemi10  7164  elfir  7171  isotilem  7204  inflbti  7222  ordiso2  7233  eldju2ndl  7270  eldju2ndr  7271  updjudhf  7277  mkvprop  7356  carden2bex  7393  pm54.43  7394  exmidfodomrlemeldju  7409  exmidfodomrlemreseldju  7410  exmidfodomrlemim  7411  pw1m  7441  ltmpig  7558  enq0sym  7651  addnq0mo  7666  mulnq0mo  7667  prarloclem3step  7715  prarloclem3  7716  genpml  7736  genpmu  7737  genprndl  7740  genprndu  7741  genpdisj  7742  distrlem1prl  7801  distrlem1pru  7802  distrlem4prl  7803  distrlem4pru  7804  distrlem5prl  7805  distrlem5pru  7806  ltsopr  7815  ltaddpr  7816  addcanprleml  7833  addcanprlemu  7834  recexprlemm  7843  recexprlemlol  7845  recexprlemupu  7847  aptiprleml  7858  aptiprlemu  7859  caucvgprlemnkj  7885  caucvgprlemnbj  7886  addsrmo  7962  mulsrmo  7963  srpospr  8002  caucvgsr  8021  axprecex  8099  mpomulf  8168  mulgt0  8253  ltne  8263  cnegexlem1  8353  cnegexlem2  8354  negf1o  8560  addgt0  8627  addgegt0  8628  addgtge0  8629  addge0  8630  recexre  8757  mulge0  8798  recexap  8832  prodgt02  9032  prodge02  9034  ltmul12a  9039  mulgt1  9042  nndivtr  9184  addltmul  9380  elnnnn0b  9445  xnn0nnn0pnf  9477  elnnz  9488  zmulcl  9532  nn0n0n1ge2  9549  nn0lt2  9560  nn0le2is012  9561  uzind2  9591  nn0ind-raph  9596  eluzp1m1  9779  uz3m2nn  9806  supinfneg  9828  infsupneg  9829  infregelbex  9831  negm  9848  lbzbi  9849  qaddcl  9868  qmulcl  9870  qreccl  9875  elpq  9882  ledivge1le  9960  nn0ledivnn  10001  xrltne  10047  xrre  10054  xrre2  10055  xrre3  10056  ge0gtmnf  10057  xltnegi  10069  xnn0xadd0  10101  xnegdi  10102  xposdif  10116  xlesubadd  10117  iccsupr  10200  icoshft  10224  icoshftf1o  10225  fznlem  10275  fzen  10277  uzsubsubfz  10281  fzsuc2  10313  elfz1b  10324  elfz0ubfz0  10359  elfz0fzfz0  10360  fz0fzelfz0  10361  fz0fzdiffz0  10364  elfzmlbp  10366  difelfznle  10369  fzofzim  10426  elincfzoext  10437  eluzgtdifelfzo  10441  elfzodifsumelfzo  10445  elfzonlteqm1  10454  elfzom1p1elfzo  10458  ssfzo12bi  10469  subfzo0  10487  zsupcllemex  10489  zssinfcl  10491  exbtwnzlemstep  10506  modqmuladdnn0  10629  modfzo0difsn  10656  addmodlteq  10659  frec2uzlt2d  10665  frecuzrdgtcl  10673  frecuzrdgfunlem  10680  seqf1og  10782  m1expcl2  10822  expge1  10837  leexp2r  10854  expubnd  10857  zesq  10919  expnlbnd  10925  nn0ltexp2  10970  nn0opthd  10983  faclbnd  11002  bcpasc  11027  hashprg  11071  seq3coll  11105  wrdnval  11143  wrdsymb0  11145  fstwrdne  11151  wrdred1hash  11156  swrdnd  11239  swrdwrdsymbg  11244  swrdsbslen  11246  swrdlsw  11249  swrdswrdlem  11284  swrdswrd  11285  pfxswrd  11286  cats1un  11301  wrd2ind  11303  swrdccatin1  11305  pfxccatin12lem4  11306  pfxccatin12lem2a  11307  pfxccatin12lem1  11308  swrdccatin2  11309  pfxccatin12lem2c  11310  pfxccatin12lem2  11311  pfxccatin12lem3  11312  pfxccatin12  11313  pfxccat3  11314  swrdccat  11315  pfxccat3a  11318  swrdccat3blem  11319  swrdccat3b  11320  swrdccatin2d  11324  reuccatpfxs1lem  11326  rexanuz  11548  rexuz3  11550  r19.29uz  11552  r19.2uz  11553  absnid  11633  leabs  11634  ltabs  11647  icodiamlt  11740  maxleast  11773  negfi  11788  climcn2  11869  climcau  11907  climcaucn  11911  sumdc  11918  fsum3cvg  11938  isumz  11949  fsumf1o  11950  fisumss  11952  isumss2  11953  fsumzcl2  11965  fsumsplit  11967  fsumsplitsnun  11979  sumsplitdc  11992  fsum2dlemstep  11994  telfsumo  12026  fsumparts  12030  fsumiun  12037  isumrpcl  12054  fproddccvg  12132  prod1dc  12146  prodssdc  12149  fprodssdc  12150  prodsnf  12152  fprodsplitdc  12156  fprod2dlemstep  12182  fprodmodd  12201  efexp  12242  efieq1re  12332  p1modz1  12354  dvds0lem  12361  dvds2ln  12384  dvdssub2  12395  dvdsadd2b  12400  dvdsabseq  12407  divconjdvds  12409  dvdsdivcl  12410  odd2np1  12433  oddge22np1  12441  opoe  12455  omoe  12456  opeo  12457  omeo  12458  m1expo  12460  nn0ehalf  12463  nn0o1gt2  12465  nno  12466  divalgb  12485  ndvdsadd  12491  bitsinv1lem  12521  gcd0id  12549  gcdneg  12552  gcdaddm  12554  bezoutlemstep  12567  dfgcd2  12584  gcddiv  12589  dvdsmulgcd  12595  bezoutr  12602  bezoutr1  12603  uzwodc  12607  nninfctlemfo  12610  algfx  12623  lcmgcdlem  12648  lcmgcdeq  12654  coprmdvds  12663  divgcdcoprmex  12673  cncongr1  12674  cncongr2  12675  isprm3  12689  dvdsnprmd  12696  prmgt1  12703  oddprmgt2  12705  isprm6  12718  cncongrprm  12728  phibndlem  12787  phimullem  12796  powm2modprm  12824  modprm0  12826  modprmn0modprm0  12828  prm23lt5  12835  pcneg  12897  pcprmpw2  12905  dvdsprmpweqnn  12908  dvdsprmpweqle  12909  pcaddlem  12911  fldivp1  12920  pcfac  12922  oddprmdvds  12926  prmunb  12934  ennnfone  13045  unct  13062  lidrididd  13464  gsummgmpropd  13476  sgrpass  13490  issgrpd  13494  issubmnd  13524  imasmnd2  13534  mnd1id  13538  insubm  13567  dfgrp2  13609  grpid  13621  grpasscan1  13645  dfgrp3mlem  13680  dfgrp3me  13682  imasgrp2  13696  mulgnn0gsum  13714  mulgnn0p1  13719  mulgaddcom  13732  mulginvcom  13733  mulgass  13745  mulgpropdg  13750  subginv  13767  issubg2m  13775  issubg4m  13779  grpissubg  13780  resgrpisgrp  13781  subgintm  13784  kerf1ghm  13860  cmncom  13888  imasabl  13922  rngdi  13952  rngdir  13953  rngpropd  13967  imasrng  13968  imasring  14076  nzrunit  14201  issubrng2  14223  subrngintm  14225  issubrg2  14254  subrgintm  14256  lmodfopnelem1  14337  lmodfopnelem2  14338  lmodfopne  14339  islssm  14370  islidlm  14492  rnglidlmcl  14493  dflidl2rng  14494  rnglidlmmgm  14509  rnglidlmsgrp  14510  rnglidlrng  14511  dvdsrzring  14616  znidom  14670  uniopn  14724  istopon  14736  fiinbas  14772  tg2  14783  tgcl  14787  0nnei  14876  tgrest  14892  tgcn  14931  cnpnei  14942  cncnp2m  14954  lmtopcnp  14973  tx2cn  14993  txcn  14998  cnmpt21  15014  isxmet2d  15071  metrest  15229  metcnpi3  15240  tgioo  15277  fsumcncntop  15290  elcncf1di  15302  climcncf  15307  cncfco  15314  suplociccreex  15347  cnplimcim  15390  cnlimci  15396  reeff1olem  15494  efltlemlt  15497  zabsle1  15727  lgslem3  15730  lgsmod  15754  lgsdir2lem5  15760  lgsdir2  15761  lgsne0  15766  lgsdirnn0  15775  gausslemma2dlem0f  15782  gausslemma2dlem1a  15786  gausslemma2dlem3  15791  2lgslem1c  15818  2lgslem3a1  15825  2lgslem3b1  15826  2lgslem3c1  15827  2lgslem3d1  15828  2lgslem3  15829  2lgsoddprmlem2  15834  uhgrm  15928  incistruhgr  15940  upgrfnen  15948  umgrfnen  15958  umgrnloop  15966  upgredgpr  15999  usgrausgrben  16022  usgredgop  16023  usgruspgrben  16036  usgrislfuspgrdom  16040  umgrvad2edg  16061  ushgredgedg  16076  ushgredgedgloop  16078  uhgr0v0e  16084  subgreldmiedg  16119  subupgr  16123  uhgrspansubgrlem  16126  vtxdg0v  16144  wlkpropg  16174  wlkvg  16178  wlkl1loop  16208  upgriswlkdc  16210  upgrwlkedg  16211  upgrwlkvtxedg  16214  uspgr2wlkeq  16215  wlkres  16229  trlf1  16238  clwwlk1loop  16249  clwwlkccatlem  16250  isclwwlknx  16266  clwwlkn1loopb  16270  clwwlkext2edg  16272  umgr2cwwk2dif  16274  clwwlknonex2lem2  16288  clwwlknonex2  16289  eupthseg  16302  bj-charfun  16402  bj-charfunr  16405  bj-charfunbi  16406  bj-prexg  16506  peano5set  16535  bj-peano4  16550  bj-nn0suc  16559  bj-nn0sucALT  16573  bj-findis  16574  exmidsbthrlem  16626  trilpolemres  16646  trirec0  16648  nconstwlpolem  16669  neapmkv  16672  gfsumval  16680