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  5489  opelf  5496  f0rn0  5520  f1oun  5592  fun11iun  5593  fv3  5650  ndmfvg  5658  fvelima  5685  fvopab3ig  5708  fvmptssdm  5719  fvmptf  5727  fvimacnv  5750  fmptco  5801  funfvima2  5872  funfvima3  5873  f1veqaeq  5893  f1ocnvfvrneq  5906  fliftfun  5920  isotr  5940  isoini  5942  isopolem  5946  isosolem  5948  moriotass  5985  acexmidlem2  5998  suppssfv  6214  suppssov1  6215  f1dmex  6261  releldm2  6331  f1o2ndf1  6374  poxp  6378  tposf2  6414  iunon  6430  smoel2  6449  tfrlem9  6465  tfrexlem  6480  tfr1onlembxssdm  6489  tfr1onlemres  6495  tfrcllembxssdm  6502  tfrcllemres  6508  tfrcl  6510  tfri3  6513  frecabcl  6545  sucinc2  6592  nnacom  6630  nnmcom  6635  nnsucsssuc  6638  nnsucuniel  6641  nntri2or2  6644  nnaordi  6654  nnmordi  6662  nnaordex  6674  nnm00  6676  ectocld  6748  iinerm  6754  th3qlem2  6785  elpm2r  6813  mapsncnv  6842  mptelixpg  6881  ixpsnf1o  6883  f1oen4g  6903  f1dom4g  6904  f1oen3g  6905  f1oeng  6908  en2d  6919  en3d  6920  dom2lem  6923  fundmen  6959  fundmeng  6960  unen  6969  rex2dom  6971  en2m  6974  xpdom2  6990  xpdom2g  6991  fopwdom  6997  nneneq  7018  phpm  7027  phpelm  7028  dif1enen  7042  fin0  7047  findcard  7050  diffifi  7056  ac6sfi  7060  onunsnss  7079  fiintim  7093  xpfi  7094  infidc  7101  fidcenum  7123  sbthlem1  7124  sbthlemi3  7126  sbthlemi10  7133  elfir  7140  isotilem  7173  inflbti  7191  ordiso2  7202  eldju2ndl  7239  eldju2ndr  7240  updjudhf  7246  mkvprop  7325  carden2bex  7362  pm54.43  7363  exmidfodomrlemeldju  7377  exmidfodomrlemreseldju  7378  exmidfodomrlemim  7379  pw1m  7409  ltmpig  7526  enq0sym  7619  addnq0mo  7634  mulnq0mo  7635  prarloclem3step  7683  prarloclem3  7684  genpml  7704  genpmu  7705  genprndl  7708  genprndu  7709  genpdisj  7710  distrlem1prl  7769  distrlem1pru  7770  distrlem4prl  7771  distrlem4pru  7772  distrlem5prl  7773  distrlem5pru  7774  ltsopr  7783  ltaddpr  7784  addcanprleml  7801  addcanprlemu  7802  recexprlemm  7811  recexprlemlol  7813  recexprlemupu  7815  aptiprleml  7826  aptiprlemu  7827  caucvgprlemnkj  7853  caucvgprlemnbj  7854  addsrmo  7930  mulsrmo  7931  srpospr  7970  caucvgsr  7989  axprecex  8067  mpomulf  8136  mulgt0  8221  ltne  8231  cnegexlem1  8321  cnegexlem2  8322  negf1o  8528  addgt0  8595  addgegt0  8596  addgtge0  8597  addge0  8598  recexre  8725  mulge0  8766  recexap  8800  prodgt02  9000  prodge02  9002  ltmul12a  9007  mulgt1  9010  nndivtr  9152  addltmul  9348  elnnnn0b  9413  xnn0nnn0pnf  9445  elnnz  9456  zmulcl  9500  nn0n0n1ge2  9517  nn0lt2  9528  nn0le2is012  9529  uzind2  9559  nn0ind-raph  9564  eluzp1m1  9746  uz3m2nn  9768  supinfneg  9790  infsupneg  9791  infregelbex  9793  negm  9810  lbzbi  9811  qaddcl  9830  qmulcl  9832  qreccl  9837  elpq  9844  ledivge1le  9922  nn0ledivnn  9963  xrltne  10009  xrre  10016  xrre2  10017  xrre3  10018  ge0gtmnf  10019  xltnegi  10031  xnn0xadd0  10063  xnegdi  10064  xposdif  10078  xlesubadd  10079  iccsupr  10162  icoshft  10186  icoshftf1o  10187  fznlem  10237  fzen  10239  uzsubsubfz  10243  fzsuc2  10275  elfz1b  10286  elfz0ubfz0  10321  elfz0fzfz0  10322  fz0fzelfz0  10323  fz0fzdiffz0  10326  elfzmlbp  10328  difelfznle  10331  fzofzim  10388  elincfzoext  10399  eluzgtdifelfzo  10403  elfzodifsumelfzo  10407  elfzonlteqm1  10416  elfzom1p1elfzo  10420  ssfzo12bi  10431  subfzo0  10448  zsupcllemex  10450  zssinfcl  10452  exbtwnzlemstep  10467  modqmuladdnn0  10590  modfzo0difsn  10617  addmodlteq  10620  frec2uzlt2d  10626  frecuzrdgtcl  10634  frecuzrdgfunlem  10641  seqf1og  10743  m1expcl2  10783  expge1  10798  leexp2r  10815  expubnd  10818  zesq  10880  expnlbnd  10886  nn0ltexp2  10931  nn0opthd  10944  faclbnd  10963  bcpasc  10988  hashprg  11030  seq3coll  11064  wrdnval  11102  wrdsymb0  11104  fstwrdne  11110  wrdred1hash  11115  swrdnd  11191  swrdwrdsymbg  11196  swrdsbslen  11198  swrdlsw  11201  swrdswrdlem  11236  swrdswrd  11237  pfxswrd  11238  cats1un  11253  wrd2ind  11255  swrdccatin1  11257  pfxccatin12lem4  11258  pfxccatin12lem2a  11259  pfxccatin12lem1  11260  swrdccatin2  11261  pfxccatin12lem2c  11262  pfxccatin12lem2  11263  pfxccatin12lem3  11264  pfxccatin12  11265  pfxccat3  11266  swrdccat  11267  pfxccat3a  11270  swrdccat3blem  11271  swrdccat3b  11272  swrdccatin2d  11276  reuccatpfxs1lem  11278  rexanuz  11499  rexuz3  11501  r19.29uz  11503  r19.2uz  11504  absnid  11584  leabs  11585  ltabs  11598  icodiamlt  11691  maxleast  11724  negfi  11739  climcn2  11820  climcau  11858  climcaucn  11862  sumdc  11869  fsum3cvg  11889  isumz  11900  fsumf1o  11901  fisumss  11903  isumss2  11904  fsumzcl2  11916  fsumsplit  11918  fsumsplitsnun  11930  sumsplitdc  11943  fsum2dlemstep  11945  telfsumo  11977  fsumparts  11981  fsumiun  11988  isumrpcl  12005  fproddccvg  12083  prod1dc  12097  prodssdc  12100  fprodssdc  12101  prodsnf  12103  fprodsplitdc  12107  fprod2dlemstep  12133  fprodmodd  12152  efexp  12193  efieq1re  12283  p1modz1  12305  dvds0lem  12312  dvds2ln  12335  dvdssub2  12346  dvdsadd2b  12351  dvdsabseq  12358  divconjdvds  12360  dvdsdivcl  12361  odd2np1  12384  oddge22np1  12392  opoe  12406  omoe  12407  opeo  12408  omeo  12409  m1expo  12411  nn0ehalf  12414  nn0o1gt2  12416  nno  12417  divalgb  12436  ndvdsadd  12442  bitsinv1lem  12472  gcd0id  12500  gcdneg  12503  gcdaddm  12505  bezoutlemstep  12518  dfgcd2  12535  gcddiv  12540  dvdsmulgcd  12546  bezoutr  12553  bezoutr1  12554  uzwodc  12558  nninfctlemfo  12561  algfx  12574  lcmgcdlem  12599  lcmgcdeq  12605  coprmdvds  12614  divgcdcoprmex  12624  cncongr1  12625  cncongr2  12626  isprm3  12640  dvdsnprmd  12647  prmgt1  12654  oddprmgt2  12656  isprm6  12669  cncongrprm  12679  phibndlem  12738  phimullem  12747  powm2modprm  12775  modprm0  12777  modprmn0modprm0  12779  prm23lt5  12786  pcneg  12848  pcprmpw2  12856  dvdsprmpweqnn  12859  dvdsprmpweqle  12860  pcaddlem  12862  fldivp1  12871  pcfac  12873  oddprmdvds  12877  prmunb  12885  ennnfone  12996  unct  13013  lidrididd  13415  gsummgmpropd  13427  sgrpass  13441  issgrpd  13445  issubmnd  13475  imasmnd2  13485  mnd1id  13489  insubm  13518  dfgrp2  13560  grpid  13572  grpasscan1  13596  dfgrp3mlem  13631  dfgrp3me  13633  imasgrp2  13647  mulgnn0gsum  13665  mulgnn0p1  13670  mulgaddcom  13683  mulginvcom  13684  mulgass  13696  mulgpropdg  13701  subginv  13718  issubg2m  13726  issubg4m  13730  grpissubg  13731  resgrpisgrp  13732  subgintm  13735  kerf1ghm  13811  cmncom  13839  imasabl  13873  rngdi  13903  rngdir  13904  rngpropd  13918  imasrng  13919  imasring  14027  nzrunit  14152  issubrng2  14174  subrngintm  14176  issubrg2  14205  subrgintm  14207  lmodfopnelem1  14288  lmodfopnelem2  14289  lmodfopne  14290  islssm  14321  islidlm  14443  rnglidlmcl  14444  dflidl2rng  14445  rnglidlmmgm  14460  rnglidlmsgrp  14461  rnglidlrng  14462  dvdsrzring  14567  znidom  14621  uniopn  14675  istopon  14687  fiinbas  14723  tg2  14734  tgcl  14738  0nnei  14827  tgrest  14843  tgcn  14882  cnpnei  14893  cncnp2m  14905  lmtopcnp  14924  tx2cn  14944  txcn  14949  cnmpt21  14965  isxmet2d  15022  metrest  15180  metcnpi3  15191  tgioo  15228  fsumcncntop  15241  elcncf1di  15253  climcncf  15258  cncfco  15265  suplociccreex  15298  cnplimcim  15341  cnlimci  15347  reeff1olem  15445  efltlemlt  15448  zabsle1  15678  lgslem3  15681  lgsmod  15705  lgsdir2lem5  15711  lgsdir2  15712  lgsne0  15717  lgsdirnn0  15726  gausslemma2dlem0f  15733  gausslemma2dlem1a  15737  gausslemma2dlem3  15742  2lgslem1c  15769  2lgslem3a1  15776  2lgslem3b1  15777  2lgslem3c1  15778  2lgslem3d1  15779  2lgslem3  15780  2lgsoddprmlem2  15785  uhgrm  15878  incistruhgr  15890  upgrfnen  15898  umgrfnen  15908  umgrnloop  15916  upgredgpr  15947  usgrausgrben  15970  usgredgop  15971  usgruspgrben  15984  usgrislfuspgrdom  15988  umgrvad2edg  16009  ushgredgedg  16024  ushgredgedgloop  16026  wlkpropg  16037  wlkvg  16040  wlkl1loop  16069  upgriswlkdc  16071  upgrwlkedg  16072  upgrwlkvtxedg  16075  uspgr2wlkeq  16076  bj-charfun  16170  bj-charfunr  16173  bj-charfunbi  16174  bj-prexg  16274  peano5set  16303  bj-peano4  16318  bj-nn0suc  16327  bj-nn0sucALT  16341  bj-findis  16342  exmidsbthrlem  16390  trilpolemres  16410  trirec0  16412  nconstwlpolem  16433  neapmkv  16436