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  602  pm3.43  604  con3dimp  638  annimim  690  imnan  694  jaoian  800  jaodan  802  stdcndc  850  impidc  863  pm2.5gdc  871  con2bidc  880  pm5.18dc  888  dfandc  889  pm4.63dc  891  pm4.54dc  907  pm4.79dc  908  orcanai  933  annimdc  943  pm4.55dc  944  orandc  945  pm4.82  956  pm3.11dc  963  pm3.12dc  964  dn1dc  966  3jcad  1202  3expia  1229  3an1rs  1243  3imp1  1244  3imp2  1246  syl3anl2  1320  3jaoian  1339  3jaodan  1340  mp3anl1  1365  mp3anl2  1366  mp3anl3  1367  ecased  1383  xor3dc  1429  pm5.15dc  1431  xor2dc  1432  xornbidc  1433  xordc  1434  nbbndc  1436  biassdc  1437  bilukdc  1438  dfbi3dc  1439  pm5.24dc  1440  xordidc  1441  alanimi  1505  19.29  1666  equs4  1771  equsexd  1775  spimth  1781  equs5a  1840  ax11v2  1866  ax11b  1872  equs5or  1876  sb5rf  1898  equvin  1909  nfsb4t  2065  eu5  2125  mopick  2156  euexex  2163  2euswapdc  2169  exists2  2175  eqrdav  2228  dvelimdc  2393  nebidc  2480  pm13.18  2481  nelne1  2490  nelne2  2491  rspa  2578  ralrimdvv  2614  r19.21bi  2618  r19.26  2657  ralbi  2663  rexbi  2664  r19.29  2668  vtoclgft  2851  rspcva  2905  rspc2va  2921  elabgt  2944  eqeu  2973  mob2  2983  mob  2985  euind  2990  reu6  2992  reuind  3008  sbctt  3095  rspsbca  3113  sbcnestgf  3176  rspcsbela  3184  ssel2  3219  sselda  3224  sstr  3232  nssne1  3282  nssne2  3283  reuss2  3484  reupick  3488  reupick2  3490  reximdva0m  3507  ssn0  3534  disjel  3546  ssdisj  3548  absneu  3738  preqr1g  3844  prel12  3849  dfiun2g  3997  nbrne1  4102  nbrne2  4103  mpteq12f  4164  triun  4195  csbexga  4212  iinexgm  4238  prexg  4295  copsex2t  4331  swopo  4397  poirr  4398  potr  4399  pofun  4403  issod  4410  ordelss  4470  trssord  4471  limelon  4490  trsuc  4513  eusvnfb  4545  rabxfrd  4560  regexmidlem1  4625  nordeq  4636  suc11g  4649  nnsuc  4708  brrelex12  4757  vtoclr  4767  optocl  4795  relop  4872  brcogw  4891  breldmg  4929  elreldm  4950  riinint  4985  issref  5111  xpidtr  5119  trin2  5120  cnveqb  5184  funopg  5352  funssres  5360  fununi  5389  funimass2  5399  imain  5403  fnun  5429  fco  5491  opelf  5498  f0rn0  5522  f1oun  5594  fun11iun  5595  fv3  5652  ndmfvg  5660  fvelima  5687  fvopab3ig  5710  fvmptssdm  5721  fvmptf  5729  fvimacnv  5752  fmptco  5803  fcof  5822  funfvima2  5876  funfvima3  5877  f1veqaeq  5899  f1ocnvfvrneq  5912  fliftfun  5926  isotr  5946  isoini  5948  isopolem  5952  isosolem  5954  moriotass  5991  acexmidlem2  6004  suppssfv  6220  suppssov1  6221  f1dmex  6267  releldm2  6337  f1o2ndf1  6380  poxp  6384  tposf2  6420  iunon  6436  smoel2  6455  tfrlem9  6471  tfrexlem  6486  tfr1onlembxssdm  6495  tfr1onlemres  6501  tfrcllembxssdm  6508  tfrcllemres  6514  tfrcl  6516  tfri3  6519  frecabcl  6551  sucinc2  6600  nnacom  6638  nnmcom  6643  nnsucsssuc  6646  nnsucuniel  6649  nntri2or2  6652  nnaordi  6662  nnmordi  6670  nnaordex  6682  nnm00  6684  ectocld  6756  iinerm  6762  th3qlem2  6793  elpm2r  6821  mapsncnv  6850  mptelixpg  6889  ixpsnf1o  6891  f1oen4g  6911  f1dom4g  6912  f1oen3g  6913  f1oeng  6916  en2d  6927  en3d  6928  dom2lem  6931  fundmen  6967  fundmeng  6968  unen  6977  rex2dom  6979  en2m  6982  xpdom2  6998  xpdom2g  6999  fopwdom  7005  nneneq  7026  phpm  7035  phpelm  7036  dif1enen  7050  fin0  7055  findcard  7058  diffifi  7064  ac6sfi  7068  onunsnss  7090  fiintim  7104  xpfi  7105  infidc  7112  fidcenum  7134  sbthlem1  7135  sbthlemi3  7137  sbthlemi10  7144  elfir  7151  isotilem  7184  inflbti  7202  ordiso2  7213  eldju2ndl  7250  eldju2ndr  7251  updjudhf  7257  mkvprop  7336  carden2bex  7373  pm54.43  7374  exmidfodomrlemeldju  7388  exmidfodomrlemreseldju  7389  exmidfodomrlemim  7390  pw1m  7420  ltmpig  7537  enq0sym  7630  addnq0mo  7645  mulnq0mo  7646  prarloclem3step  7694  prarloclem3  7695  genpml  7715  genpmu  7716  genprndl  7719  genprndu  7720  genpdisj  7721  distrlem1prl  7780  distrlem1pru  7781  distrlem4prl  7782  distrlem4pru  7783  distrlem5prl  7784  distrlem5pru  7785  ltsopr  7794  ltaddpr  7795  addcanprleml  7812  addcanprlemu  7813  recexprlemm  7822  recexprlemlol  7824  recexprlemupu  7826  aptiprleml  7837  aptiprlemu  7838  caucvgprlemnkj  7864  caucvgprlemnbj  7865  addsrmo  7941  mulsrmo  7942  srpospr  7981  caucvgsr  8000  axprecex  8078  mpomulf  8147  mulgt0  8232  ltne  8242  cnegexlem1  8332  cnegexlem2  8333  negf1o  8539  addgt0  8606  addgegt0  8607  addgtge0  8608  addge0  8609  recexre  8736  mulge0  8777  recexap  8811  prodgt02  9011  prodge02  9013  ltmul12a  9018  mulgt1  9021  nndivtr  9163  addltmul  9359  elnnnn0b  9424  xnn0nnn0pnf  9456  elnnz  9467  zmulcl  9511  nn0n0n1ge2  9528  nn0lt2  9539  nn0le2is012  9540  uzind2  9570  nn0ind-raph  9575  eluzp1m1  9758  uz3m2nn  9780  supinfneg  9802  infsupneg  9803  infregelbex  9805  negm  9822  lbzbi  9823  qaddcl  9842  qmulcl  9844  qreccl  9849  elpq  9856  ledivge1le  9934  nn0ledivnn  9975  xrltne  10021  xrre  10028  xrre2  10029  xrre3  10030  ge0gtmnf  10031  xltnegi  10043  xnn0xadd0  10075  xnegdi  10076  xposdif  10090  xlesubadd  10091  iccsupr  10174  icoshft  10198  icoshftf1o  10199  fznlem  10249  fzen  10251  uzsubsubfz  10255  fzsuc2  10287  elfz1b  10298  elfz0ubfz0  10333  elfz0fzfz0  10334  fz0fzelfz0  10335  fz0fzdiffz0  10338  elfzmlbp  10340  difelfznle  10343  fzofzim  10400  elincfzoext  10411  eluzgtdifelfzo  10415  elfzodifsumelfzo  10419  elfzonlteqm1  10428  elfzom1p1elfzo  10432  ssfzo12bi  10443  subfzo0  10460  zsupcllemex  10462  zssinfcl  10464  exbtwnzlemstep  10479  modqmuladdnn0  10602  modfzo0difsn  10629  addmodlteq  10632  frec2uzlt2d  10638  frecuzrdgtcl  10646  frecuzrdgfunlem  10653  seqf1og  10755  m1expcl2  10795  expge1  10810  leexp2r  10827  expubnd  10830  zesq  10892  expnlbnd  10898  nn0ltexp2  10943  nn0opthd  10956  faclbnd  10975  bcpasc  11000  hashprg  11043  seq3coll  11077  wrdnval  11115  wrdsymb0  11117  fstwrdne  11123  wrdred1hash  11128  swrdnd  11207  swrdwrdsymbg  11212  swrdsbslen  11214  swrdlsw  11217  swrdswrdlem  11252  swrdswrd  11253  pfxswrd  11254  cats1un  11269  wrd2ind  11271  swrdccatin1  11273  pfxccatin12lem4  11274  pfxccatin12lem2a  11275  pfxccatin12lem1  11276  swrdccatin2  11277  pfxccatin12lem2c  11278  pfxccatin12lem2  11279  pfxccatin12lem3  11280  pfxccatin12  11281  pfxccat3  11282  swrdccat  11283  pfxccat3a  11286  swrdccat3blem  11287  swrdccat3b  11288  swrdccatin2d  11292  reuccatpfxs1lem  11294  rexanuz  11515  rexuz3  11517  r19.29uz  11519  r19.2uz  11520  absnid  11600  leabs  11601  ltabs  11614  icodiamlt  11707  maxleast  11740  negfi  11755  climcn2  11836  climcau  11874  climcaucn  11878  sumdc  11885  fsum3cvg  11905  isumz  11916  fsumf1o  11917  fisumss  11919  isumss2  11920  fsumzcl2  11932  fsumsplit  11934  fsumsplitsnun  11946  sumsplitdc  11959  fsum2dlemstep  11961  telfsumo  11993  fsumparts  11997  fsumiun  12004  isumrpcl  12021  fproddccvg  12099  prod1dc  12113  prodssdc  12116  fprodssdc  12117  prodsnf  12119  fprodsplitdc  12123  fprod2dlemstep  12149  fprodmodd  12168  efexp  12209  efieq1re  12299  p1modz1  12321  dvds0lem  12328  dvds2ln  12351  dvdssub2  12362  dvdsadd2b  12367  dvdsabseq  12374  divconjdvds  12376  dvdsdivcl  12377  odd2np1  12400  oddge22np1  12408  opoe  12422  omoe  12423  opeo  12424  omeo  12425  m1expo  12427  nn0ehalf  12430  nn0o1gt2  12432  nno  12433  divalgb  12452  ndvdsadd  12458  bitsinv1lem  12488  gcd0id  12516  gcdneg  12519  gcdaddm  12521  bezoutlemstep  12534  dfgcd2  12551  gcddiv  12556  dvdsmulgcd  12562  bezoutr  12569  bezoutr1  12570  uzwodc  12574  nninfctlemfo  12577  algfx  12590  lcmgcdlem  12615  lcmgcdeq  12621  coprmdvds  12630  divgcdcoprmex  12640  cncongr1  12641  cncongr2  12642  isprm3  12656  dvdsnprmd  12663  prmgt1  12670  oddprmgt2  12672  isprm6  12685  cncongrprm  12695  phibndlem  12754  phimullem  12763  powm2modprm  12791  modprm0  12793  modprmn0modprm0  12795  prm23lt5  12802  pcneg  12864  pcprmpw2  12872  dvdsprmpweqnn  12875  dvdsprmpweqle  12876  pcaddlem  12878  fldivp1  12887  pcfac  12889  oddprmdvds  12893  prmunb  12901  ennnfone  13012  unct  13029  lidrididd  13431  gsummgmpropd  13443  sgrpass  13457  issgrpd  13461  issubmnd  13491  imasmnd2  13501  mnd1id  13505  insubm  13534  dfgrp2  13576  grpid  13588  grpasscan1  13612  dfgrp3mlem  13647  dfgrp3me  13649  imasgrp2  13663  mulgnn0gsum  13681  mulgnn0p1  13686  mulgaddcom  13699  mulginvcom  13700  mulgass  13712  mulgpropdg  13717  subginv  13734  issubg2m  13742  issubg4m  13746  grpissubg  13747  resgrpisgrp  13748  subgintm  13751  kerf1ghm  13827  cmncom  13855  imasabl  13889  rngdi  13919  rngdir  13920  rngpropd  13934  imasrng  13935  imasring  14043  nzrunit  14168  issubrng2  14190  subrngintm  14192  issubrg2  14221  subrgintm  14223  lmodfopnelem1  14304  lmodfopnelem2  14305  lmodfopne  14306  islssm  14337  islidlm  14459  rnglidlmcl  14460  dflidl2rng  14461  rnglidlmmgm  14476  rnglidlmsgrp  14477  rnglidlrng  14478  dvdsrzring  14583  znidom  14637  uniopn  14691  istopon  14703  fiinbas  14739  tg2  14750  tgcl  14754  0nnei  14843  tgrest  14859  tgcn  14898  cnpnei  14909  cncnp2m  14921  lmtopcnp  14940  tx2cn  14960  txcn  14965  cnmpt21  14981  isxmet2d  15038  metrest  15196  metcnpi3  15207  tgioo  15244  fsumcncntop  15257  elcncf1di  15269  climcncf  15274  cncfco  15281  suplociccreex  15314  cnplimcim  15357  cnlimci  15363  reeff1olem  15461  efltlemlt  15464  zabsle1  15694  lgslem3  15697  lgsmod  15721  lgsdir2lem5  15727  lgsdir2  15728  lgsne0  15733  lgsdirnn0  15742  gausslemma2dlem0f  15749  gausslemma2dlem1a  15753  gausslemma2dlem3  15758  2lgslem1c  15785  2lgslem3a1  15792  2lgslem3b1  15793  2lgslem3c1  15794  2lgslem3d1  15795  2lgslem3  15796  2lgsoddprmlem2  15801  uhgrm  15894  incistruhgr  15906  upgrfnen  15914  umgrfnen  15924  umgrnloop  15932  upgredgpr  15963  usgrausgrben  15986  usgredgop  15987  usgruspgrben  16000  usgrislfuspgrdom  16004  umgrvad2edg  16025  ushgredgedg  16040  ushgredgedgloop  16042  vtxdg0v  16054  wlkpropg  16070  wlkvg  16074  wlkl1loop  16104  upgriswlkdc  16106  upgrwlkedg  16107  upgrwlkvtxedg  16110  uspgr2wlkeq  16111  wlkres  16123  trlf1  16131  clwwlk1loop  16142  clwwlkccatlem  16143  isclwwlknx  16158  clwwlkn1loopb  16162  clwwlkext2edg  16164  umgr2cwwk2dif  16166  bj-charfun  16253  bj-charfunr  16256  bj-charfunbi  16257  bj-prexg  16357  peano5set  16386  bj-peano4  16401  bj-nn0suc  16410  bj-nn0sucALT  16424  bj-findis  16425  exmidsbthrlem  16478  trilpolemres  16498  trirec0  16500  nconstwlpolem  16521  neapmkv  16524