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  688  imnan  692  jaoian  797  jaodan  799  stdcndc  847  impidc  860  pm2.5gdc  868  con2bidc  877  pm5.18dc  885  dfandc  886  pm4.63dc  888  pm4.54dc  904  pm4.79dc  905  orcanai  930  annimdc  940  pm4.55dc  941  orandc  942  pm4.82  953  pm3.11dc  960  pm3.12dc  961  dn1dc  963  3jcad  1181  3expia  1208  3an1rs  1222  3imp1  1223  3imp2  1225  syl3anl2  1299  3jaoian  1318  3jaodan  1319  mp3anl1  1344  mp3anl2  1345  mp3anl3  1346  ecased  1362  xor3dc  1407  pm5.15dc  1409  xor2dc  1410  xornbidc  1411  xordc  1412  nbbndc  1414  biassdc  1415  bilukdc  1416  dfbi3dc  1417  pm5.24dc  1418  xordidc  1419  alanimi  1483  19.29  1644  equs4  1749  equsexd  1753  spimth  1759  equs5a  1818  ax11v2  1844  ax11b  1850  equs5or  1854  sb5rf  1876  equvin  1887  nfsb4t  2043  eu5  2103  mopick  2134  euexex  2141  2euswapdc  2147  exists2  2153  eqrdav  2206  dvelimdc  2371  nebidc  2458  pm13.18  2459  nelne1  2468  nelne2  2469  rspa  2556  ralrimdvv  2592  r19.21bi  2596  r19.26  2634  ralbi  2640  rexbi  2641  r19.29  2645  vtoclgft  2828  rspcva  2882  rspc2va  2898  elabgt  2921  eqeu  2950  mob2  2960  mob  2962  euind  2967  reu6  2969  reuind  2985  sbctt  3072  rspsbca  3090  sbcnestgf  3153  rspcsbela  3161  ssel2  3196  sselda  3201  sstr  3209  nssne1  3259  nssne2  3260  reuss2  3461  reupick  3465  reupick2  3467  reximdva0m  3484  ssn0  3511  disjel  3523  ssdisj  3525  absneu  3715  preqr1g  3820  prel12  3825  dfiun2g  3973  nbrne1  4078  nbrne2  4079  mpteq12f  4140  triun  4171  csbexga  4188  iinexgm  4214  prexg  4271  copsex2t  4307  swopo  4371  poirr  4372  potr  4373  pofun  4377  issod  4384  ordelss  4444  trssord  4445  limelon  4464  trsuc  4487  eusvnfb  4519  rabxfrd  4534  regexmidlem1  4599  nordeq  4610  suc11g  4623  nnsuc  4682  brrelex12  4731  vtoclr  4741  optocl  4769  relop  4846  brcogw  4865  breldmg  4903  elreldm  4923  riinint  4958  issref  5084  xpidtr  5092  trin2  5093  cnveqb  5157  funopg  5324  funssres  5332  fununi  5361  funimass2  5371  imain  5375  fnun  5401  fco  5461  opelf  5468  f0rn0  5492  f1oun  5564  fun11iun  5565  fv3  5622  ndmfvg  5630  fvelima  5653  fvopab3ig  5676  fvmptssdm  5687  fvmptf  5695  fvimacnv  5718  fmptco  5769  funfvima2  5840  funfvima3  5841  f1veqaeq  5861  f1ocnvfvrneq  5874  fliftfun  5888  isotr  5908  isoini  5910  isopolem  5914  isosolem  5916  moriotass  5951  acexmidlem2  5964  suppssfv  6177  suppssov1  6178  f1dmex  6224  releldm2  6294  f1o2ndf1  6337  poxp  6341  tposf2  6377  iunon  6393  smoel2  6412  tfrlem9  6428  tfrexlem  6443  tfr1onlembxssdm  6452  tfr1onlemres  6458  tfrcllembxssdm  6465  tfrcllemres  6471  tfrcl  6473  tfri3  6476  frecabcl  6508  sucinc2  6555  nnacom  6593  nnmcom  6598  nnsucsssuc  6601  nnsucuniel  6604  nntri2or2  6607  nnaordi  6617  nnmordi  6625  nnaordex  6637  nnm00  6639  ectocld  6711  iinerm  6717  th3qlem2  6748  elpm2r  6776  mapsncnv  6805  mptelixpg  6844  ixpsnf1o  6846  f1oen4g  6866  f1dom4g  6867  f1oen3g  6868  f1oeng  6871  en2d  6882  en3d  6883  dom2lem  6886  fundmen  6922  fundmeng  6923  unen  6932  rex2dom  6934  en2m  6937  xpdom2  6951  xpdom2g  6952  fopwdom  6958  nneneq  6979  phpm  6988  phpelm  6989  dif1enen  7003  fin0  7008  findcard  7011  diffifi  7017  ac6sfi  7021  onunsnss  7040  fiintim  7054  xpfi  7055  infidc  7062  fidcenum  7084  sbthlem1  7085  sbthlemi3  7087  sbthlemi10  7094  elfir  7101  isotilem  7134  inflbti  7152  ordiso2  7163  eldju2ndl  7200  eldju2ndr  7201  updjudhf  7207  mkvprop  7286  carden2bex  7323  pm54.43  7324  exmidfodomrlemeldju  7338  exmidfodomrlemreseldju  7339  exmidfodomrlemim  7340  pw1m  7370  ltmpig  7487  enq0sym  7580  addnq0mo  7595  mulnq0mo  7596  prarloclem3step  7644  prarloclem3  7645  genpml  7665  genpmu  7666  genprndl  7669  genprndu  7670  genpdisj  7671  distrlem1prl  7730  distrlem1pru  7731  distrlem4prl  7732  distrlem4pru  7733  distrlem5prl  7734  distrlem5pru  7735  ltsopr  7744  ltaddpr  7745  addcanprleml  7762  addcanprlemu  7763  recexprlemm  7772  recexprlemlol  7774  recexprlemupu  7776  aptiprleml  7787  aptiprlemu  7788  caucvgprlemnkj  7814  caucvgprlemnbj  7815  addsrmo  7891  mulsrmo  7892  srpospr  7931  caucvgsr  7950  axprecex  8028  mpomulf  8097  mulgt0  8182  ltne  8192  cnegexlem1  8282  cnegexlem2  8283  negf1o  8489  addgt0  8556  addgegt0  8557  addgtge0  8558  addge0  8559  recexre  8686  mulge0  8727  recexap  8761  prodgt02  8961  prodge02  8963  ltmul12a  8968  mulgt1  8971  nndivtr  9113  addltmul  9309  elnnnn0b  9374  xnn0nnn0pnf  9406  elnnz  9417  zmulcl  9461  nn0n0n1ge2  9478  nn0lt2  9489  nn0le2is012  9490  uzind2  9520  nn0ind-raph  9525  eluzp1m1  9707  uz3m2nn  9729  supinfneg  9751  infsupneg  9752  infregelbex  9754  negm  9771  lbzbi  9772  qaddcl  9791  qmulcl  9793  qreccl  9798  elpq  9805  ledivge1le  9883  nn0ledivnn  9924  xrltne  9970  xrre  9977  xrre2  9978  xrre3  9979  ge0gtmnf  9980  xltnegi  9992  xnn0xadd0  10024  xnegdi  10025  xposdif  10039  xlesubadd  10040  iccsupr  10123  icoshft  10147  icoshftf1o  10148  fznlem  10198  fzen  10200  uzsubsubfz  10204  fzsuc2  10236  elfz1b  10247  elfz0ubfz0  10282  elfz0fzfz0  10283  fz0fzelfz0  10284  fz0fzdiffz0  10287  elfzmlbp  10289  difelfznle  10292  fzofzim  10349  elincfzoext  10359  eluzgtdifelfzo  10363  elfzodifsumelfzo  10367  elfzonlteqm1  10376  elfzom1p1elfzo  10380  ssfzo12bi  10391  subfzo0  10408  zsupcllemex  10410  zssinfcl  10412  exbtwnzlemstep  10427  modqmuladdnn0  10550  modfzo0difsn  10577  addmodlteq  10580  frec2uzlt2d  10586  frecuzrdgtcl  10594  frecuzrdgfunlem  10601  seqf1og  10703  m1expcl2  10743  expge1  10758  leexp2r  10775  expubnd  10778  zesq  10840  expnlbnd  10846  nn0ltexp2  10891  nn0opthd  10904  faclbnd  10923  bcpasc  10948  hashprg  10990  seq3coll  11024  wrdnval  11061  wrdsymb0  11063  fstwrdne  11069  wrdred1hash  11074  swrdnd  11150  swrdwrdsymbg  11155  swrdsbslen  11157  swrdlsw  11160  swrdswrdlem  11195  swrdswrd  11196  pfxswrd  11197  cats1un  11212  wrd2ind  11214  swrdccatin1  11216  pfxccatin12lem4  11217  pfxccatin12lem2a  11218  pfxccatin12lem1  11219  swrdccatin2  11220  pfxccatin12lem2c  11221  pfxccatin12lem2  11222  pfxccatin12lem3  11223  pfxccatin12  11224  pfxccat3  11225  swrdccat  11226  pfxccat3a  11229  swrdccat3blem  11230  swrdccat3b  11231  swrdccatin2d  11235  reuccatpfxs1lem  11237  rexanuz  11414  rexuz3  11416  r19.29uz  11418  r19.2uz  11419  absnid  11499  leabs  11500  ltabs  11513  icodiamlt  11606  maxleast  11639  negfi  11654  climcn2  11735  climcau  11773  climcaucn  11777  sumdc  11784  fsum3cvg  11804  isumz  11815  fsumf1o  11816  fisumss  11818  isumss2  11819  fsumzcl2  11831  fsumsplit  11833  fsumsplitsnun  11845  sumsplitdc  11858  fsum2dlemstep  11860  telfsumo  11892  fsumparts  11896  fsumiun  11903  isumrpcl  11920  fproddccvg  11998  prod1dc  12012  prodssdc  12015  fprodssdc  12016  prodsnf  12018  fprodsplitdc  12022  fprod2dlemstep  12048  fprodmodd  12067  efexp  12108  efieq1re  12198  p1modz1  12220  dvds0lem  12227  dvds2ln  12250  dvdssub2  12261  dvdsadd2b  12266  dvdsabseq  12273  divconjdvds  12275  dvdsdivcl  12276  odd2np1  12299  oddge22np1  12307  opoe  12321  omoe  12322  opeo  12323  omeo  12324  m1expo  12326  nn0ehalf  12329  nn0o1gt2  12331  nno  12332  divalgb  12351  ndvdsadd  12357  bitsinv1lem  12387  gcd0id  12415  gcdneg  12418  gcdaddm  12420  bezoutlemstep  12433  dfgcd2  12450  gcddiv  12455  dvdsmulgcd  12461  bezoutr  12468  bezoutr1  12469  uzwodc  12473  nninfctlemfo  12476  algfx  12489  lcmgcdlem  12514  lcmgcdeq  12520  coprmdvds  12529  divgcdcoprmex  12539  cncongr1  12540  cncongr2  12541  isprm3  12555  dvdsnprmd  12562  prmgt1  12569  oddprmgt2  12571  isprm6  12584  cncongrprm  12594  phibndlem  12653  phimullem  12662  powm2modprm  12690  modprm0  12692  modprmn0modprm0  12694  prm23lt5  12701  pcneg  12763  pcprmpw2  12771  dvdsprmpweqnn  12774  dvdsprmpweqle  12775  pcaddlem  12777  fldivp1  12786  pcfac  12788  oddprmdvds  12792  prmunb  12800  ennnfone  12911  unct  12928  lidrididd  13329  gsummgmpropd  13341  sgrpass  13355  issgrpd  13359  issubmnd  13389  imasmnd2  13399  mnd1id  13403  insubm  13432  dfgrp2  13474  grpid  13486  grpasscan1  13510  dfgrp3mlem  13545  dfgrp3me  13547  imasgrp2  13561  mulgnn0gsum  13579  mulgnn0p1  13584  mulgaddcom  13597  mulginvcom  13598  mulgass  13610  mulgpropdg  13615  subginv  13632  issubg2m  13640  issubg4m  13644  grpissubg  13645  resgrpisgrp  13646  subgintm  13649  kerf1ghm  13725  cmncom  13753  imasabl  13787  rngdi  13817  rngdir  13818  rngpropd  13832  imasrng  13833  imasring  13941  nzrunit  14065  issubrng2  14087  subrngintm  14089  issubrg2  14118  subrgintm  14120  lmodfopnelem1  14201  lmodfopnelem2  14202  lmodfopne  14203  islssm  14234  islidlm  14356  rnglidlmcl  14357  dflidl2rng  14358  rnglidlmmgm  14373  rnglidlmsgrp  14374  rnglidlrng  14375  dvdsrzring  14480  znidom  14534  uniopn  14588  istopon  14600  fiinbas  14636  tg2  14647  tgcl  14651  0nnei  14740  tgrest  14756  tgcn  14795  cnpnei  14806  cncnp2m  14818  lmtopcnp  14837  tx2cn  14857  txcn  14862  cnmpt21  14878  isxmet2d  14935  metrest  15093  metcnpi3  15104  tgioo  15141  fsumcncntop  15154  elcncf1di  15166  climcncf  15171  cncfco  15178  suplociccreex  15211  cnplimcim  15254  cnlimci  15260  reeff1olem  15358  efltlemlt  15361  zabsle1  15591  lgslem3  15594  lgsmod  15618  lgsdir2lem5  15624  lgsdir2  15625  lgsne0  15630  lgsdirnn0  15639  gausslemma2dlem0f  15646  gausslemma2dlem1a  15650  gausslemma2dlem3  15655  2lgslem1c  15682  2lgslem3a1  15689  2lgslem3b1  15690  2lgslem3c1  15691  2lgslem3d1  15692  2lgslem3  15693  2lgsoddprmlem2  15698  uhgrm  15789  incistruhgr  15801  upgrfnen  15809  umgrfnen  15819  upgredgpr  15853  bj-charfun  15942  bj-charfunr  15945  bj-charfunbi  15946  bj-prexg  16046  peano5set  16075  bj-peano4  16090  bj-nn0suc  16099  bj-nn0sucALT  16113  bj-findis  16114  exmidsbthrlem  16163  trilpolemres  16183  trirec0  16185  nconstwlpolem  16206  neapmkv  16209