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  2852  rspcva  2906  rspc2va  2922  elabgt  2945  eqeu  2974  mob2  2984  mob  2986  euind  2991  reu6  2993  reuind  3009  sbctt  3096  rspsbca  3114  sbcnestgf  3177  rspcsbela  3185  ssel2  3220  sselda  3225  sstr  3233  nssne1  3283  nssne2  3284  reuss2  3485  reupick  3489  reupick2  3491  reximdva0m  3508  ssn0  3535  disjel  3547  ssdisj  3549  absneu  3741  preqr1g  3847  prel12  3852  dfiun2g  4000  nbrne1  4105  nbrne2  4106  mpteq12f  4167  triun  4198  csbexga  4215  prcssprc  4228  iinexgm  4242  prexg  4299  copsex2t  4335  swopo  4401  poirr  4402  potr  4403  pofun  4407  issod  4414  ordelss  4474  trssord  4475  limelon  4494  trsuc  4517  eusvnfb  4549  rabxfrd  4564  regexmidlem1  4629  nordeq  4640  suc11g  4653  nnsuc  4712  brrelex12  4762  vtoclr  4772  optocl  4800  relop  4878  brcogw  4897  breldmg  4935  elreldm  4956  riinint  4991  issref  5117  xpidtr  5125  trin2  5126  cnveqb  5190  funopg  5358  funssres  5366  fununi  5395  funimass2  5405  imain  5409  fnun  5435  fco  5497  opelf  5504  f0rn0  5528  f1oun  5600  fun11iun  5601  fv3  5658  ndmfvg  5666  fvelima  5693  fvopab3ig  5716  fvmptssdm  5727  fvmptf  5735  fvimacnv  5758  fmptco  5809  fcof  5828  funfvima2  5882  funfvima3  5883  f1veqaeq  5905  f1ocnvfvrneq  5918  fliftfun  5932  isotr  5952  isoini  5954  isopolem  5958  isosolem  5960  moriotass  5997  acexmidlem2  6010  suppssfv  6226  suppssov1  6227  f1dmex  6273  releldm2  6343  f1o2ndf1  6388  poxp  6392  tposf2  6429  iunon  6445  smoel2  6464  tfrlem9  6480  tfrexlem  6495  tfr1onlembxssdm  6504  tfr1onlemres  6510  tfrcllembxssdm  6517  tfrcllemres  6523  tfrcl  6525  tfri3  6528  frecabcl  6560  sucinc2  6609  nnacom  6647  nnmcom  6652  nnsucsssuc  6655  nnsucuniel  6658  nntri2or2  6661  nnaordi  6671  nnmordi  6679  nnaordex  6691  nnm00  6693  ectocld  6765  iinerm  6771  th3qlem2  6802  elpm2r  6830  mapsncnv  6859  mptelixpg  6898  ixpsnf1o  6900  f1oen4g  6920  f1dom4g  6921  f1oen3g  6922  f1oeng  6925  en2d  6936  en3d  6937  dom2lem  6940  fundmen  6976  fundmeng  6977  unen  6986  modom  6989  rex2dom  6991  en2m  6994  xpdom2  7010  xpdom2g  7011  fopwdom  7017  nneneq  7038  phpm  7047  phpelm  7048  dif1enen  7062  fin0  7067  findcard  7070  diffifi  7076  ac6sfi  7080  onunsnss  7102  fiintim  7116  xpfi  7117  infidc  7124  fidcenum  7146  sbthlem1  7147  sbthlemi3  7149  sbthlemi10  7156  elfir  7163  isotilem  7196  inflbti  7214  ordiso2  7225  eldju2ndl  7262  eldju2ndr  7263  updjudhf  7269  mkvprop  7348  carden2bex  7385  pm54.43  7386  exmidfodomrlemeldju  7400  exmidfodomrlemreseldju  7401  exmidfodomrlemim  7402  pw1m  7432  ltmpig  7549  enq0sym  7642  addnq0mo  7657  mulnq0mo  7658  prarloclem3step  7706  prarloclem3  7707  genpml  7727  genpmu  7728  genprndl  7731  genprndu  7732  genpdisj  7733  distrlem1prl  7792  distrlem1pru  7793  distrlem4prl  7794  distrlem4pru  7795  distrlem5prl  7796  distrlem5pru  7797  ltsopr  7806  ltaddpr  7807  addcanprleml  7824  addcanprlemu  7825  recexprlemm  7834  recexprlemlol  7836  recexprlemupu  7838  aptiprleml  7849  aptiprlemu  7850  caucvgprlemnkj  7876  caucvgprlemnbj  7877  addsrmo  7953  mulsrmo  7954  srpospr  7993  caucvgsr  8012  axprecex  8090  mpomulf  8159  mulgt0  8244  ltne  8254  cnegexlem1  8344  cnegexlem2  8345  negf1o  8551  addgt0  8618  addgegt0  8619  addgtge0  8620  addge0  8621  recexre  8748  mulge0  8789  recexap  8823  prodgt02  9023  prodge02  9025  ltmul12a  9030  mulgt1  9033  nndivtr  9175  addltmul  9371  elnnnn0b  9436  xnn0nnn0pnf  9468  elnnz  9479  zmulcl  9523  nn0n0n1ge2  9540  nn0lt2  9551  nn0le2is012  9552  uzind2  9582  nn0ind-raph  9587  eluzp1m1  9770  uz3m2nn  9797  supinfneg  9819  infsupneg  9820  infregelbex  9822  negm  9839  lbzbi  9840  qaddcl  9859  qmulcl  9861  qreccl  9866  elpq  9873  ledivge1le  9951  nn0ledivnn  9992  xrltne  10038  xrre  10045  xrre2  10046  xrre3  10047  ge0gtmnf  10048  xltnegi  10060  xnn0xadd0  10092  xnegdi  10093  xposdif  10107  xlesubadd  10108  iccsupr  10191  icoshft  10215  icoshftf1o  10216  fznlem  10266  fzen  10268  uzsubsubfz  10272  fzsuc2  10304  elfz1b  10315  elfz0ubfz0  10350  elfz0fzfz0  10351  fz0fzelfz0  10352  fz0fzdiffz0  10355  elfzmlbp  10357  difelfznle  10360  fzofzim  10417  elincfzoext  10428  eluzgtdifelfzo  10432  elfzodifsumelfzo  10436  elfzonlteqm1  10445  elfzom1p1elfzo  10449  ssfzo12bi  10460  subfzo0  10478  zsupcllemex  10480  zssinfcl  10482  exbtwnzlemstep  10497  modqmuladdnn0  10620  modfzo0difsn  10647  addmodlteq  10650  frec2uzlt2d  10656  frecuzrdgtcl  10664  frecuzrdgfunlem  10671  seqf1og  10773  m1expcl2  10813  expge1  10828  leexp2r  10845  expubnd  10848  zesq  10910  expnlbnd  10916  nn0ltexp2  10961  nn0opthd  10974  faclbnd  10993  bcpasc  11018  hashprg  11062  seq3coll  11096  wrdnval  11134  wrdsymb0  11136  fstwrdne  11142  wrdred1hash  11147  swrdnd  11230  swrdwrdsymbg  11235  swrdsbslen  11237  swrdlsw  11240  swrdswrdlem  11275  swrdswrd  11276  pfxswrd  11277  cats1un  11292  wrd2ind  11294  swrdccatin1  11296  pfxccatin12lem4  11297  pfxccatin12lem2a  11298  pfxccatin12lem1  11299  swrdccatin2  11300  pfxccatin12lem2c  11301  pfxccatin12lem2  11302  pfxccatin12lem3  11303  pfxccatin12  11304  pfxccat3  11305  swrdccat  11306  pfxccat3a  11309  swrdccat3blem  11310  swrdccat3b  11311  swrdccatin2d  11315  reuccatpfxs1lem  11317  rexanuz  11539  rexuz3  11541  r19.29uz  11543  r19.2uz  11544  absnid  11624  leabs  11625  ltabs  11638  icodiamlt  11731  maxleast  11764  negfi  11779  climcn2  11860  climcau  11898  climcaucn  11902  sumdc  11909  fsum3cvg  11929  isumz  11940  fsumf1o  11941  fisumss  11943  isumss2  11944  fsumzcl2  11956  fsumsplit  11958  fsumsplitsnun  11970  sumsplitdc  11983  fsum2dlemstep  11985  telfsumo  12017  fsumparts  12021  fsumiun  12028  isumrpcl  12045  fproddccvg  12123  prod1dc  12137  prodssdc  12140  fprodssdc  12141  prodsnf  12143  fprodsplitdc  12147  fprod2dlemstep  12173  fprodmodd  12192  efexp  12233  efieq1re  12323  p1modz1  12345  dvds0lem  12352  dvds2ln  12375  dvdssub2  12386  dvdsadd2b  12391  dvdsabseq  12398  divconjdvds  12400  dvdsdivcl  12401  odd2np1  12424  oddge22np1  12432  opoe  12446  omoe  12447  opeo  12448  omeo  12449  m1expo  12451  nn0ehalf  12454  nn0o1gt2  12456  nno  12457  divalgb  12476  ndvdsadd  12482  bitsinv1lem  12512  gcd0id  12540  gcdneg  12543  gcdaddm  12545  bezoutlemstep  12558  dfgcd2  12575  gcddiv  12580  dvdsmulgcd  12586  bezoutr  12593  bezoutr1  12594  uzwodc  12598  nninfctlemfo  12601  algfx  12614  lcmgcdlem  12639  lcmgcdeq  12645  coprmdvds  12654  divgcdcoprmex  12664  cncongr1  12665  cncongr2  12666  isprm3  12680  dvdsnprmd  12687  prmgt1  12694  oddprmgt2  12696  isprm6  12709  cncongrprm  12719  phibndlem  12778  phimullem  12787  powm2modprm  12815  modprm0  12817  modprmn0modprm0  12819  prm23lt5  12826  pcneg  12888  pcprmpw2  12896  dvdsprmpweqnn  12899  dvdsprmpweqle  12900  pcaddlem  12902  fldivp1  12911  pcfac  12913  oddprmdvds  12917  prmunb  12925  ennnfone  13036  unct  13053  lidrididd  13455  gsummgmpropd  13467  sgrpass  13481  issgrpd  13485  issubmnd  13515  imasmnd2  13525  mnd1id  13529  insubm  13558  dfgrp2  13600  grpid  13612  grpasscan1  13636  dfgrp3mlem  13671  dfgrp3me  13673  imasgrp2  13687  mulgnn0gsum  13705  mulgnn0p1  13710  mulgaddcom  13723  mulginvcom  13724  mulgass  13736  mulgpropdg  13741  subginv  13758  issubg2m  13766  issubg4m  13770  grpissubg  13771  resgrpisgrp  13772  subgintm  13775  kerf1ghm  13851  cmncom  13879  imasabl  13913  rngdi  13943  rngdir  13944  rngpropd  13958  imasrng  13959  imasring  14067  nzrunit  14192  issubrng2  14214  subrngintm  14216  issubrg2  14245  subrgintm  14247  lmodfopnelem1  14328  lmodfopnelem2  14329  lmodfopne  14330  islssm  14361  islidlm  14483  rnglidlmcl  14484  dflidl2rng  14485  rnglidlmmgm  14500  rnglidlmsgrp  14501  rnglidlrng  14502  dvdsrzring  14607  znidom  14661  uniopn  14715  istopon  14727  fiinbas  14763  tg2  14774  tgcl  14778  0nnei  14867  tgrest  14883  tgcn  14922  cnpnei  14933  cncnp2m  14945  lmtopcnp  14964  tx2cn  14984  txcn  14989  cnmpt21  15005  isxmet2d  15062  metrest  15220  metcnpi3  15231  tgioo  15268  fsumcncntop  15281  elcncf1di  15293  climcncf  15298  cncfco  15305  suplociccreex  15338  cnplimcim  15381  cnlimci  15387  reeff1olem  15485  efltlemlt  15488  zabsle1  15718  lgslem3  15721  lgsmod  15745  lgsdir2lem5  15751  lgsdir2  15752  lgsne0  15757  lgsdirnn0  15766  gausslemma2dlem0f  15773  gausslemma2dlem1a  15777  gausslemma2dlem3  15782  2lgslem1c  15809  2lgslem3a1  15816  2lgslem3b1  15817  2lgslem3c1  15818  2lgslem3d1  15819  2lgslem3  15820  2lgsoddprmlem2  15825  uhgrm  15919  incistruhgr  15931  upgrfnen  15939  umgrfnen  15949  umgrnloop  15957  upgredgpr  15988  usgrausgrben  16011  usgredgop  16012  usgruspgrben  16025  usgrislfuspgrdom  16029  umgrvad2edg  16050  ushgredgedg  16065  ushgredgedgloop  16067  uhgr0v0e  16073  vtxdg0v  16100  wlkpropg  16121  wlkvg  16125  wlkl1loop  16155  upgriswlkdc  16157  upgrwlkedg  16158  upgrwlkvtxedg  16161  uspgr2wlkeq  16162  wlkres  16174  trlf1  16183  clwwlk1loop  16194  clwwlkccatlem  16195  isclwwlknx  16211  clwwlkn1loopb  16215  clwwlkext2edg  16217  umgr2cwwk2dif  16219  clwwlknonex2lem2  16233  clwwlknonex2  16234  eupthseg  16247  bj-charfun  16338  bj-charfunr  16341  bj-charfunbi  16342  bj-prexg  16442  peano5set  16471  bj-peano4  16486  bj-nn0suc  16495  bj-nn0sucALT  16509  bj-findis  16510  exmidsbthrlem  16562  trilpolemres  16582  trirec0  16584  nconstwlpolem  16605  neapmkv  16608