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  2102  mopick  2133  euexex  2140  2euswapdc  2146  exists2  2152  eqrdav  2205  dvelimdc  2370  nebidc  2457  pm13.18  2458  nelne1  2467  nelne2  2468  rspa  2555  ralrimdvv  2591  r19.21bi  2595  r19.26  2633  ralbi  2639  rexbi  2640  r19.29  2644  vtoclgft  2825  rspcva  2879  rspc2va  2895  elabgt  2918  eqeu  2947  mob2  2957  mob  2959  euind  2964  reu6  2966  reuind  2982  sbctt  3069  rspsbca  3086  sbcnestgf  3149  rspcsbela  3157  ssel2  3192  sselda  3197  sstr  3205  nssne1  3255  nssne2  3256  reuss2  3457  reupick  3461  reupick2  3463  reximdva0m  3480  ssn0  3507  disjel  3519  ssdisj  3521  absneu  3710  preqr1g  3813  prel12  3818  dfiun2g  3965  nbrne1  4070  nbrne2  4071  mpteq12f  4132  triun  4163  csbexga  4180  iinexgm  4206  prexg  4263  copsex2t  4297  swopo  4361  poirr  4362  potr  4363  pofun  4367  issod  4374  ordelss  4434  trssord  4435  limelon  4454  trsuc  4477  eusvnfb  4509  rabxfrd  4524  regexmidlem1  4589  nordeq  4600  suc11g  4613  nnsuc  4672  brrelex12  4721  vtoclr  4731  optocl  4759  relop  4836  brcogw  4855  breldmg  4893  elreldm  4913  riinint  4948  issref  5074  xpidtr  5082  trin2  5083  cnveqb  5147  funopg  5314  funssres  5322  fununi  5351  funimass2  5361  imain  5365  fnun  5391  fco  5451  opelf  5458  f0rn0  5482  f1oun  5554  fun11iun  5555  fv3  5612  ndmfvg  5620  fvelima  5643  fvopab3ig  5666  fvmptssdm  5677  fvmptf  5685  fvimacnv  5708  fmptco  5759  funfvima2  5830  funfvima3  5831  f1veqaeq  5851  f1ocnvfvrneq  5864  fliftfun  5878  isotr  5898  isoini  5900  isopolem  5904  isosolem  5906  moriotass  5941  acexmidlem2  5954  suppssfv  6167  suppssov1  6168  f1dmex  6214  releldm2  6284  f1o2ndf1  6327  poxp  6331  tposf2  6367  iunon  6383  smoel2  6402  tfrlem9  6418  tfrexlem  6433  tfr1onlembxssdm  6442  tfr1onlemres  6448  tfrcllembxssdm  6455  tfrcllemres  6461  tfrcl  6463  tfri3  6466  frecabcl  6498  sucinc2  6545  nnacom  6583  nnmcom  6588  nnsucsssuc  6591  nnsucuniel  6594  nntri2or2  6597  nnaordi  6607  nnmordi  6615  nnaordex  6627  nnm00  6629  ectocld  6701  iinerm  6707  th3qlem2  6738  elpm2r  6766  mapsncnv  6795  mptelixpg  6834  ixpsnf1o  6836  f1oen4g  6856  f1dom4g  6857  f1oen3g  6858  f1oeng  6861  en2d  6872  en3d  6873  dom2lem  6876  fundmen  6912  fundmeng  6913  unen  6922  rex2dom  6924  en2m  6927  xpdom2  6941  xpdom2g  6942  fopwdom  6948  nneneq  6969  phpm  6977  phpelm  6978  dif1enen  6992  fin0  6997  findcard  7000  diffifi  7006  ac6sfi  7010  onunsnss  7029  fiintim  7043  xpfi  7044  infidc  7051  fidcenum  7073  sbthlem1  7074  sbthlemi3  7076  sbthlemi10  7083  elfir  7090  isotilem  7123  inflbti  7141  ordiso2  7152  eldju2ndl  7189  eldju2ndr  7190  updjudhf  7196  mkvprop  7275  carden2bex  7312  pm54.43  7313  exmidfodomrlemeldju  7323  exmidfodomrlemreseldju  7324  exmidfodomrlemim  7325  pw1m  7355  ltmpig  7472  enq0sym  7565  addnq0mo  7580  mulnq0mo  7581  prarloclem3step  7629  prarloclem3  7630  genpml  7650  genpmu  7651  genprndl  7654  genprndu  7655  genpdisj  7656  distrlem1prl  7715  distrlem1pru  7716  distrlem4prl  7717  distrlem4pru  7718  distrlem5prl  7719  distrlem5pru  7720  ltsopr  7729  ltaddpr  7730  addcanprleml  7747  addcanprlemu  7748  recexprlemm  7757  recexprlemlol  7759  recexprlemupu  7761  aptiprleml  7772  aptiprlemu  7773  caucvgprlemnkj  7799  caucvgprlemnbj  7800  addsrmo  7876  mulsrmo  7877  srpospr  7916  caucvgsr  7935  axprecex  8013  mpomulf  8082  mulgt0  8167  ltne  8177  cnegexlem1  8267  cnegexlem2  8268  negf1o  8474  addgt0  8541  addgegt0  8542  addgtge0  8543  addge0  8544  recexre  8671  mulge0  8712  recexap  8746  prodgt02  8946  prodge02  8948  ltmul12a  8953  mulgt1  8956  nndivtr  9098  addltmul  9294  elnnnn0b  9359  xnn0nnn0pnf  9391  elnnz  9402  zmulcl  9446  nn0n0n1ge2  9463  nn0lt2  9474  nn0le2is012  9475  uzind2  9505  nn0ind-raph  9510  eluzp1m1  9692  uz3m2nn  9714  supinfneg  9736  infsupneg  9737  infregelbex  9739  negm  9756  lbzbi  9757  qaddcl  9776  qmulcl  9778  qreccl  9783  elpq  9790  ledivge1le  9868  nn0ledivnn  9909  xrltne  9955  xrre  9962  xrre2  9963  xrre3  9964  ge0gtmnf  9965  xltnegi  9977  xnn0xadd0  10009  xnegdi  10010  xposdif  10024  xlesubadd  10025  iccsupr  10108  icoshft  10132  icoshftf1o  10133  fznlem  10183  fzen  10185  uzsubsubfz  10189  fzsuc2  10221  elfz1b  10232  elfz0ubfz0  10267  elfz0fzfz0  10268  fz0fzelfz0  10269  fz0fzdiffz0  10272  elfzmlbp  10274  difelfznle  10277  fzofzim  10334  elincfzoext  10344  eluzgtdifelfzo  10348  elfzodifsumelfzo  10352  elfzonlteqm1  10361  elfzom1p1elfzo  10365  ssfzo12bi  10376  subfzo0  10393  zsupcllemex  10395  zssinfcl  10397  exbtwnzlemstep  10412  modqmuladdnn0  10535  modfzo0difsn  10562  addmodlteq  10565  frec2uzlt2d  10571  frecuzrdgtcl  10579  frecuzrdgfunlem  10586  seqf1og  10688  m1expcl2  10728  expge1  10743  leexp2r  10760  expubnd  10763  zesq  10825  expnlbnd  10831  nn0ltexp2  10876  nn0opthd  10889  faclbnd  10908  bcpasc  10933  hashprg  10975  seq3coll  11009  wrdnval  11046  wrdsymb0  11048  fstwrdne  11054  wrdred1hash  11059  swrdnd  11135  swrdwrdsymbg  11140  swrdsbslen  11142  swrdlsw  11145  swrdswrdlem  11180  swrdswrd  11181  pfxswrd  11182  cats1un  11197  wrd2ind  11199  rexanuz  11374  rexuz3  11376  r19.29uz  11378  r19.2uz  11379  absnid  11459  leabs  11460  ltabs  11473  icodiamlt  11566  maxleast  11599  negfi  11614  climcn2  11695  climcau  11733  climcaucn  11737  sumdc  11744  fsum3cvg  11764  isumz  11775  fsumf1o  11776  fisumss  11778  isumss2  11779  fsumzcl2  11791  fsumsplit  11793  fsumsplitsnun  11805  sumsplitdc  11818  fsum2dlemstep  11820  telfsumo  11852  fsumparts  11856  fsumiun  11863  isumrpcl  11880  fproddccvg  11958  prod1dc  11972  prodssdc  11975  fprodssdc  11976  prodsnf  11978  fprodsplitdc  11982  fprod2dlemstep  12008  fprodmodd  12027  efexp  12068  efieq1re  12158  p1modz1  12180  dvds0lem  12187  dvds2ln  12210  dvdssub2  12221  dvdsadd2b  12226  dvdsabseq  12233  divconjdvds  12235  dvdsdivcl  12236  odd2np1  12259  oddge22np1  12267  opoe  12281  omoe  12282  opeo  12283  omeo  12284  m1expo  12286  nn0ehalf  12289  nn0o1gt2  12291  nno  12292  divalgb  12311  ndvdsadd  12317  bitsinv1lem  12347  gcd0id  12375  gcdneg  12378  gcdaddm  12380  bezoutlemstep  12393  dfgcd2  12410  gcddiv  12415  dvdsmulgcd  12421  bezoutr  12428  bezoutr1  12429  uzwodc  12433  nninfctlemfo  12436  algfx  12449  lcmgcdlem  12474  lcmgcdeq  12480  coprmdvds  12489  divgcdcoprmex  12499  cncongr1  12500  cncongr2  12501  isprm3  12515  dvdsnprmd  12522  prmgt1  12529  oddprmgt2  12531  isprm6  12544  cncongrprm  12554  phibndlem  12613  phimullem  12622  powm2modprm  12650  modprm0  12652  modprmn0modprm0  12654  prm23lt5  12661  pcneg  12723  pcprmpw2  12731  dvdsprmpweqnn  12734  dvdsprmpweqle  12735  pcaddlem  12737  fldivp1  12746  pcfac  12748  oddprmdvds  12752  prmunb  12760  ennnfone  12871  unct  12888  lidrididd  13289  gsummgmpropd  13301  sgrpass  13315  issgrpd  13319  issubmnd  13349  imasmnd2  13359  mnd1id  13363  insubm  13392  dfgrp2  13434  grpid  13446  grpasscan1  13470  dfgrp3mlem  13505  dfgrp3me  13507  imasgrp2  13521  mulgnn0gsum  13539  mulgnn0p1  13544  mulgaddcom  13557  mulginvcom  13558  mulgass  13570  mulgpropdg  13575  subginv  13592  issubg2m  13600  issubg4m  13604  grpissubg  13605  resgrpisgrp  13606  subgintm  13609  kerf1ghm  13685  cmncom  13713  imasabl  13747  rngdi  13777  rngdir  13778  rngpropd  13792  imasrng  13793  imasring  13901  nzrunit  14025  issubrng2  14047  subrngintm  14049  issubrg2  14078  subrgintm  14080  lmodfopnelem1  14161  lmodfopnelem2  14162  lmodfopne  14163  islssm  14194  islidlm  14316  rnglidlmcl  14317  dflidl2rng  14318  rnglidlmmgm  14333  rnglidlmsgrp  14334  rnglidlrng  14335  dvdsrzring  14440  znidom  14494  uniopn  14548  istopon  14560  fiinbas  14596  tg2  14607  tgcl  14611  0nnei  14700  tgrest  14716  tgcn  14755  cnpnei  14766  cncnp2m  14778  lmtopcnp  14797  tx2cn  14817  txcn  14822  cnmpt21  14838  isxmet2d  14895  metrest  15053  metcnpi3  15064  tgioo  15101  fsumcncntop  15114  elcncf1di  15126  climcncf  15131  cncfco  15138  suplociccreex  15171  cnplimcim  15214  cnlimci  15220  reeff1olem  15318  efltlemlt  15321  zabsle1  15551  lgslem3  15554  lgsmod  15578  lgsdir2lem5  15584  lgsdir2  15585  lgsne0  15590  lgsdirnn0  15599  gausslemma2dlem0f  15606  gausslemma2dlem1a  15610  gausslemma2dlem3  15615  2lgslem1c  15642  2lgslem3a1  15649  2lgslem3b1  15650  2lgslem3c1  15651  2lgslem3d1  15652  2lgslem3  15653  2lgsoddprmlem2  15658  uhgrm  15749  incistruhgr  15761  upgrfnen  15769  umgrfnen  15779  bj-charfun  15881  bj-charfunr  15884  bj-charfunbi  15885  bj-prexg  15985  peano5set  16014  bj-peano4  16029  bj-nn0suc  16038  bj-nn0sucALT  16052  bj-findis  16053  exmidsbthrlem  16102  trilpolemres  16122  trirec0  16124  nconstwlpolem  16145  neapmkv  16148