Theorem imp 123

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 108	. 2 |- ( ( ph /\ ps ) -> ph )
2		simpr 109	. 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 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem is referenced by:  impcom  124  impd  252  imp31  254  imp32  255  expdimp  257  impancom  258  pm3.22  263  ancoms  266  adantr  274  impel  278  biimpa  294  biimpar  295  biimpac  296  biimparc  297  pm3.33  343  pm3.34  344  pm3.35  345  pm5.31  346  imp4b  348  imp41  351  imp42  352  imp43  353  imp44  354  imp45  355  imp5g  358  expr  373  impac  379  sylan9  407  sylan9r  408  imdistani  442  mpan10  466  adantl4r  509  adantl5r  517  adantl6r  518  a2and  548  anabsi5  569  anim12dan  590  pm3.43  592  con3dimp  625  annimim  676  imnan  680  jaoian  785  jaodan  787  stdcndc  835  impidc  848  pm2.5gdc  856  con2bidc  865  pm5.18dc  873  dfandc  874  pm4.63dc  876  pm4.54dc  892  pm4.79dc  893  orcanai  918  annimdc  927  pm4.55dc  928  orandc  929  pm4.82  940  pm3.11dc  947  pm3.12dc  948  dn1dc  950  3jcad  1168  3expia  1195  3an1rs  1209  3imp1  1210  3imp2  1212  syl3anl2  1277  3jaoian  1295  3jaodan  1296  mp3anl1  1321  mp3anl2  1322  mp3anl3  1323  ecased  1339  xor3dc  1377  pm5.15dc  1379  xor2dc  1380  xornbidc  1381  xordc  1382  nbbndc  1384  biassdc  1385  bilukdc  1386  dfbi3dc  1387  pm5.24dc  1388  xordidc  1389  alanimi  1447  19.29  1608  equs4  1713  equsexd  1717  spimth  1723  equs5a  1782  ax11v2  1808  ax11b  1814  equs5or  1818  sb5rf  1840  equvin  1851  nfsb4t  2002  eu5  2061  mopick  2092  euexex  2099  2euswapdc  2105  exists2  2111  eqrdav  2164  dvelimdc  2329  nebidc  2416  pm13.18  2417  nelne1  2426  nelne2  2427  rspa  2514  ralrimdvv  2550  r19.21bi  2554  r19.26  2592  ralbi  2598  rexbi  2599  r19.29  2603  vtoclgft  2776  rspcva  2828  rspc2va  2844  elabgt  2867  eqeu  2896  mob2  2906  mob  2908  euind  2913  reu6  2915  reuind  2931  sbctt  3017  rspsbca  3034  sbcnestgf  3096  rspcsbela  3104  ssel2  3137  sselda  3142  sstr  3150  nssne1  3200  nssne2  3201  reuss2  3402  reupick  3406  reupick2  3408  reximdva0m  3424  ssn0  3451  disjel  3463  ssdisj  3465  absneu  3648  preqr1g  3746  prel12  3751  dfiun2g  3898  nbrne1  4001  nbrne2  4002  mpteq12f  4062  triun  4093  csbexga  4110  iinexgm  4133  prexg  4189  copsex2t  4223  swopo  4284  poirr  4285  potr  4286  pofun  4290  issod  4297  ordelss  4357  trssord  4358  limelon  4377  trsuc  4400  eusvnfb  4432  rabxfrd  4447  regexmidlem1  4510  nordeq  4521  suc11g  4534  nnsuc  4593  brrelex12  4642  vtoclr  4652  optocl  4680  relop  4754  brcogw  4773  breldmg  4810  elreldm  4830  riinint  4865  issref  4986  xpidtr  4994  trin2  4995  cnveqb  5059  funopg  5222  funssres  5230  fununi  5256  funimass2  5266  imain  5270  fnun  5294  fco  5353  opelf  5359  f0rn0  5382  f1oun  5452  fun11iun  5453  fv3  5509  ndmfvg  5517  fvelima  5538  fvopab3ig  5560  fvmptssdm  5570  fvmptf  5578  fvimacnv  5600  fmptco  5651  funfvima2  5717  funfvima3  5718  f1veqaeq  5737  f1ocnvfvrneq  5750  fliftfun  5764  isotr  5784  isoini  5786  isopolem  5790  isosolem  5792  moriotass  5826  acexmidlem2  5839  suppssfv  6046  suppssov1  6047  f1dmex  6084  releldm2  6153  f1o2ndf1  6196  poxp  6200  tposf2  6236  iunon  6252  smoel2  6271  tfrlem9  6287  tfrexlem  6302  tfr1onlembxssdm  6311  tfr1onlemres  6317  tfrcllembxssdm  6324  tfrcllemres  6330  tfrcl  6332  tfri3  6335  frecabcl  6367  sucinc2  6414  nnacom  6452  nnmcom  6457  nnsucsssuc  6460  nnsucuniel  6463  nntri2or2  6466  nnaordi  6476  nnmordi  6484  nnaordex  6495  nnm00  6497  ectocld  6567  iinerm  6573  th3qlem2  6604  elpm2r  6632  mapsncnv  6661  mptelixpg  6700  ixpsnf1o  6702  f1oen3g  6720  f1oeng  6723  en2d  6734  en3d  6735  dom2lem  6738  fundmen  6772  fundmeng  6773  unen  6782  xpdom2  6797  xpdom2g  6798  fopwdom  6802  nneneq  6823  phpm  6831  phpelm  6832  dif1enen  6846  fin0  6851  findcard  6854  diffifi  6860  ac6sfi  6864  onunsnss  6882  fiintim  6894  xpfi  6895  fidcenum  6921  sbthlem1  6922  sbthlemi3  6924  sbthlemi10  6931  elfir  6938  isotilem  6971  inflbti  6989  ordiso2  7000  eldju2ndl  7037  eldju2ndr  7038  updjudhf  7044  mkvprop  7122  carden2bex  7145  pm54.43  7146  exmidfodomrlemeldju  7155  exmidfodomrlemreseldju  7156  exmidfodomrlemim  7157  ltmpig  7280  enq0sym  7373  addnq0mo  7388  mulnq0mo  7389  prarloclem3step  7437  prarloclem3  7438  genpml  7458  genpmu  7459  genprndl  7462  genprndu  7463  genpdisj  7464  distrlem1prl  7523  distrlem1pru  7524  distrlem4prl  7525  distrlem4pru  7526  distrlem5prl  7527  distrlem5pru  7528  ltsopr  7537  ltaddpr  7538  addcanprleml  7555  addcanprlemu  7556  recexprlemm  7565  recexprlemlol  7567  recexprlemupu  7569  aptiprleml  7580  aptiprlemu  7581  caucvgprlemnkj  7607  caucvgprlemnbj  7608  addsrmo  7684  mulsrmo  7685  srpospr  7724  caucvgsr  7743  axprecex  7821  mulgt0  7973  ltne  7983  cnegexlem1  8073  cnegexlem2  8074  negf1o  8280  addgt0  8346  addgegt0  8347  addgtge0  8348  addge0  8349  recexre  8476  mulge0  8517  recexap  8550  prodgt02  8748  prodge02  8750  ltmul12a  8755  mulgt1  8758  nndivtr  8899  addltmul  9093  elnnnn0b  9158  xnn0nnn0pnf  9190  elnnz  9201  zmulcl  9244  nn0n0n1ge2  9261  nn0lt2  9272  nn0le2is012  9273  uzind2  9303  nn0ind-raph  9308  eluzp1m1  9489  uz3m2nn  9511  supinfneg  9533  infsupneg  9534  infregelbex  9536  negm  9553  lbzbi  9554  qaddcl  9573  qmulcl  9575  qreccl  9580  elpq  9586  ledivge1le  9662  nn0ledivnn  9703  xrltne  9749  xrre  9756  xrre2  9757  xrre3  9758  ge0gtmnf  9759  xltnegi  9771  xnn0xadd0  9803  xnegdi  9804  xposdif  9818  xlesubadd  9819  iccsupr  9902  icoshft  9926  icoshftf1o  9927  fznlem  9976  fzen  9978  uzsubsubfz  9982  fzsuc2  10014  elfz1b  10025  elfz0ubfz0  10060  elfz0fzfz0  10061  fz0fzelfz0  10062  fz0fzdiffz0  10065  elfzmlbp  10067  difelfznle  10070  fzofzim  10123  eluzgtdifelfzo  10132  elfzodifsumelfzo  10136  elfzonlteqm1  10145  elfzom1p1elfzo  10149  ssfzo12bi  10160  subfzo0  10177  exbtwnzlemstep  10183  modqmuladdnn0  10303  modfzo0difsn  10330  addmodlteq  10333  frec2uzlt2d  10339  frecuzrdgtcl  10347  frecuzrdgfunlem  10354  m1expcl2  10477  expge1  10492  leexp2r  10509  expubnd  10512  zesq  10573  expnlbnd  10579  nn0ltexp2  10623  nn0opthd  10635  faclbnd  10654  bcpasc  10679  hashprg  10721  seq3coll  10755  rexanuz  10930  rexuz3  10932  r19.29uz  10934  r19.2uz  10935  absnid  11015  leabs  11016  ltabs  11029  icodiamlt  11122  maxleast  11155  negfi  11169  climcn2  11250  climcau  11288  climcaucn  11292  sumdc  11299  fsum3cvg  11319  isumz  11330  fsumf1o  11331  fisumss  11333  isumss2  11334  fsumzcl2  11346  fsumsplit  11348  fsumsplitsnun  11360  sumsplitdc  11373  fsum2dlemstep  11375  telfsumo  11407  fsumparts  11411  fsumiun  11418  isumrpcl  11435  fproddccvg  11513  prod1dc  11527  prodssdc  11530  fprodssdc  11531  prodsnf  11533  fprodsplitdc  11537  fprod2dlemstep  11563  fprodmodd  11582  efexp  11623  efieq1re  11712  p1modz1  11734  dvds0lem  11741  dvds2ln  11764  dvdssub2  11775  dvdsadd2b  11780  dvdsabseq  11785  divconjdvds  11787  dvdsdivcl  11788  odd2np1  11810  oddge22np1  11818  opoe  11832  omoe  11833  opeo  11834  omeo  11835  m1expo  11837  nn0ehalf  11840  nn0o1gt2  11842  nno  11843  divalgb  11862  ndvdsadd  11868  zsupcllemex  11879  zssinfcl  11881  gcd0id  11912  gcdneg  11915  gcdaddm  11917  bezoutlemstep  11930  dfgcd2  11947  gcddiv  11952  dvdsmulgcd  11958  bezoutr  11965  bezoutr1  11966  uzwodc  11970  algfx  11984  lcmgcdlem  12009  lcmgcdeq  12015  coprmdvds  12024  divgcdcoprmex  12034  cncongr1  12035  cncongr2  12036  isprm3  12050  dvdsnprmd  12057  prmgt1  12064  oddprmgt2  12066  isprm6  12079  cncongrprm  12089  phibndlem  12148  phimullem  12157  powm2modprm  12184  modprm0  12186  modprmn0modprm0  12188  prm23lt5  12195  pcneg  12256  pcprmpw2  12264  dvdsprmpweqnn  12267  dvdsprmpweqle  12268  pcaddlem  12270  fldivp1  12278  pcfac  12280  oddprmdvds  12284  prmunb  12292  ennnfone  12358  unct  12375  lidrididd  12613  uniopn  12639  istopon  12651  fiinbas  12687  tg2  12700  tgcl  12704  0nnei  12793  tgrest  12809  tgcn  12848  cnpnei  12859  cncnp2m  12871  lmtopcnp  12890  tx2cn  12910  txcn  12915  cnmpt21  12931  isxmet2d  12988  metrest  13146  metcnpi3  13157  tgioo  13186  fsumcncntop  13196  elcncf1di  13206  climcncf  13211  cncfco  13218  suplociccreex  13242  cnplimcim  13276  cnlimci  13282  reeff1olem  13332  efltlemlt  13335  zabsle1  13540  lgslem3  13543  lgsmod  13567  lgsdir2lem5  13573  lgsdir2  13574  lgsne0  13579  lgsdirnn0  13588  bj-charfun  13689  bj-charfunr  13692  bj-charfunbi  13693  bj-prexg  13793  peano5set  13822  bj-peano4  13837  bj-nn0suc  13846  bj-nn0sucALT  13860  bj-findis  13861  exmidsbthrlem  13901  trilpolemres  13921  trirec0  13923  nconstwlpolem  13943  neapmkv  13946