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  635  annimim  686  imnan  690  jaoian  795  jaodan  797  stdcndc  845  impidc  858  pm2.5gdc  866  con2bidc  875  pm5.18dc  883  dfandc  884  pm4.63dc  886  pm4.54dc  902  pm4.79dc  903  orcanai  928  annimdc  937  pm4.55dc  938  orandc  939  pm4.82  950  pm3.11dc  957  pm3.12dc  958  dn1dc  960  3jcad  1178  3expia  1205  3an1rs  1219  3imp1  1220  3imp2  1222  syl3anl2  1287  3jaoian  1305  3jaodan  1306  mp3anl1  1331  mp3anl2  1332  mp3anl3  1333  ecased  1349  xor3dc  1387  pm5.15dc  1389  xor2dc  1390  xornbidc  1391  xordc  1392  nbbndc  1394  biassdc  1395  bilukdc  1396  dfbi3dc  1397  pm5.24dc  1398  xordidc  1399  alanimi  1457  19.29  1618  equs4  1723  equsexd  1727  spimth  1733  equs5a  1792  ax11v2  1818  ax11b  1824  equs5or  1828  sb5rf  1850  equvin  1861  nfsb4t  2012  eu5  2071  mopick  2102  euexex  2109  2euswapdc  2115  exists2  2121  eqrdav  2174  dvelimdc  2338  nebidc  2425  pm13.18  2426  nelne1  2435  nelne2  2436  rspa  2523  ralrimdvv  2559  r19.21bi  2563  r19.26  2601  ralbi  2607  rexbi  2608  r19.29  2612  vtoclgft  2785  rspcva  2837  rspc2va  2853  elabgt  2876  eqeu  2905  mob2  2915  mob  2917  euind  2922  reu6  2924  reuind  2940  sbctt  3027  rspsbca  3044  sbcnestgf  3106  rspcsbela  3114  ssel2  3148  sselda  3153  sstr  3161  nssne1  3211  nssne2  3212  reuss2  3413  reupick  3417  reupick2  3419  reximdva0m  3436  ssn0  3463  disjel  3475  ssdisj  3477  absneu  3661  preqr1g  3762  prel12  3767  dfiun2g  3914  nbrne1  4017  nbrne2  4018  mpteq12f  4078  triun  4109  csbexga  4126  iinexgm  4149  prexg  4205  copsex2t  4239  swopo  4300  poirr  4301  potr  4302  pofun  4306  issod  4313  ordelss  4373  trssord  4374  limelon  4393  trsuc  4416  eusvnfb  4448  rabxfrd  4463  regexmidlem1  4526  nordeq  4537  suc11g  4550  nnsuc  4609  brrelex12  4658  vtoclr  4668  optocl  4696  relop  4770  brcogw  4789  breldmg  4826  elreldm  4846  riinint  4881  issref  5003  xpidtr  5011  trin2  5012  cnveqb  5076  funopg  5242  funssres  5250  fununi  5276  funimass2  5286  imain  5290  fnun  5314  fco  5373  opelf  5379  f0rn0  5402  f1oun  5473  fun11iun  5474  fv3  5530  ndmfvg  5538  fvelima  5559  fvopab3ig  5582  fvmptssdm  5592  fvmptf  5600  fvimacnv  5623  fmptco  5674  funfvima2  5740  funfvima3  5741  f1veqaeq  5760  f1ocnvfvrneq  5773  fliftfun  5787  isotr  5807  isoini  5809  isopolem  5813  isosolem  5815  moriotass  5849  acexmidlem2  5862  suppssfv  6069  suppssov1  6070  f1dmex  6107  releldm2  6176  f1o2ndf1  6219  poxp  6223  tposf2  6259  iunon  6275  smoel2  6294  tfrlem9  6310  tfrexlem  6325  tfr1onlembxssdm  6334  tfr1onlemres  6340  tfrcllembxssdm  6347  tfrcllemres  6353  tfrcl  6355  tfri3  6358  frecabcl  6390  sucinc2  6437  nnacom  6475  nnmcom  6480  nnsucsssuc  6483  nnsucuniel  6486  nntri2or2  6489  nnaordi  6499  nnmordi  6507  nnaordex  6519  nnm00  6521  ectocld  6591  iinerm  6597  th3qlem2  6628  elpm2r  6656  mapsncnv  6685  mptelixpg  6724  ixpsnf1o  6726  f1oen3g  6744  f1oeng  6747  en2d  6758  en3d  6759  dom2lem  6762  fundmen  6796  fundmeng  6797  unen  6806  xpdom2  6821  xpdom2g  6822  fopwdom  6826  nneneq  6847  phpm  6855  phpelm  6856  dif1enen  6870  fin0  6875  findcard  6878  diffifi  6884  ac6sfi  6888  onunsnss  6906  fiintim  6918  xpfi  6919  fidcenum  6945  sbthlem1  6946  sbthlemi3  6948  sbthlemi10  6955  elfir  6962  isotilem  6995  inflbti  7013  ordiso2  7024  eldju2ndl  7061  eldju2ndr  7062  updjudhf  7068  mkvprop  7146  carden2bex  7178  pm54.43  7179  exmidfodomrlemeldju  7188  exmidfodomrlemreseldju  7189  exmidfodomrlemim  7190  ltmpig  7313  enq0sym  7406  addnq0mo  7421  mulnq0mo  7422  prarloclem3step  7470  prarloclem3  7471  genpml  7491  genpmu  7492  genprndl  7495  genprndu  7496  genpdisj  7497  distrlem1prl  7556  distrlem1pru  7557  distrlem4prl  7558  distrlem4pru  7559  distrlem5prl  7560  distrlem5pru  7561  ltsopr  7570  ltaddpr  7571  addcanprleml  7588  addcanprlemu  7589  recexprlemm  7598  recexprlemlol  7600  recexprlemupu  7602  aptiprleml  7613  aptiprlemu  7614  caucvgprlemnkj  7640  caucvgprlemnbj  7641  addsrmo  7717  mulsrmo  7718  srpospr  7757  caucvgsr  7776  axprecex  7854  mulgt0  8006  ltne  8016  cnegexlem1  8106  cnegexlem2  8107  negf1o  8313  addgt0  8379  addgegt0  8380  addgtge0  8381  addge0  8382  recexre  8509  mulge0  8550  recexap  8583  prodgt02  8783  prodge02  8785  ltmul12a  8790  mulgt1  8793  nndivtr  8934  addltmul  9128  elnnnn0b  9193  xnn0nnn0pnf  9225  elnnz  9236  zmulcl  9279  nn0n0n1ge2  9296  nn0lt2  9307  nn0le2is012  9308  uzind2  9338  nn0ind-raph  9343  eluzp1m1  9524  uz3m2nn  9546  supinfneg  9568  infsupneg  9569  infregelbex  9571  negm  9588  lbzbi  9589  qaddcl  9608  qmulcl  9610  qreccl  9615  elpq  9621  ledivge1le  9697  nn0ledivnn  9738  xrltne  9784  xrre  9791  xrre2  9792  xrre3  9793  ge0gtmnf  9794  xltnegi  9806  xnn0xadd0  9838  xnegdi  9839  xposdif  9853  xlesubadd  9854  iccsupr  9937  icoshft  9961  icoshftf1o  9962  fznlem  10011  fzen  10013  uzsubsubfz  10017  fzsuc2  10049  elfz1b  10060  elfz0ubfz0  10095  elfz0fzfz0  10096  fz0fzelfz0  10097  fz0fzdiffz0  10100  elfzmlbp  10102  difelfznle  10105  fzofzim  10158  eluzgtdifelfzo  10167  elfzodifsumelfzo  10171  elfzonlteqm1  10180  elfzom1p1elfzo  10184  ssfzo12bi  10195  subfzo0  10212  exbtwnzlemstep  10218  modqmuladdnn0  10338  modfzo0difsn  10365  addmodlteq  10368  frec2uzlt2d  10374  frecuzrdgtcl  10382  frecuzrdgfunlem  10389  m1expcl2  10512  expge1  10527  leexp2r  10544  expubnd  10547  zesq  10608  expnlbnd  10614  nn0ltexp2  10658  nn0opthd  10670  faclbnd  10689  bcpasc  10714  hashprg  10756  seq3coll  10790  rexanuz  10965  rexuz3  10967  r19.29uz  10969  r19.2uz  10970  absnid  11050  leabs  11051  ltabs  11064  icodiamlt  11157  maxleast  11190  negfi  11204  climcn2  11285  climcau  11323  climcaucn  11327  sumdc  11334  fsum3cvg  11354  isumz  11365  fsumf1o  11366  fisumss  11368  isumss2  11369  fsumzcl2  11381  fsumsplit  11383  fsumsplitsnun  11395  sumsplitdc  11408  fsum2dlemstep  11410  telfsumo  11442  fsumparts  11446  fsumiun  11453  isumrpcl  11470  fproddccvg  11548  prod1dc  11562  prodssdc  11565  fprodssdc  11566  prodsnf  11568  fprodsplitdc  11572  fprod2dlemstep  11598  fprodmodd  11617  efexp  11658  efieq1re  11747  p1modz1  11769  dvds0lem  11776  dvds2ln  11799  dvdssub2  11810  dvdsadd2b  11815  dvdsabseq  11820  divconjdvds  11822  dvdsdivcl  11823  odd2np1  11845  oddge22np1  11853  opoe  11867  omoe  11868  opeo  11869  omeo  11870  m1expo  11872  nn0ehalf  11875  nn0o1gt2  11877  nno  11878  divalgb  11897  ndvdsadd  11903  zsupcllemex  11914  zssinfcl  11916  gcd0id  11947  gcdneg  11950  gcdaddm  11952  bezoutlemstep  11965  dfgcd2  11982  gcddiv  11987  dvdsmulgcd  11993  bezoutr  12000  bezoutr1  12001  uzwodc  12005  algfx  12019  lcmgcdlem  12044  lcmgcdeq  12050  coprmdvds  12059  divgcdcoprmex  12069  cncongr1  12070  cncongr2  12071  isprm3  12085  dvdsnprmd  12092  prmgt1  12099  oddprmgt2  12101  isprm6  12114  cncongrprm  12124  phibndlem  12183  phimullem  12192  powm2modprm  12219  modprm0  12221  modprmn0modprm0  12223  prm23lt5  12230  pcneg  12291  pcprmpw2  12299  dvdsprmpweqnn  12302  dvdsprmpweqle  12303  pcaddlem  12305  fldivp1  12313  pcfac  12315  oddprmdvds  12319  prmunb  12327  ennnfone  12393  unct  12410  lidrididd  12667  sgrpass  12680  mnd1id  12711  insubm  12734  dfgrp2  12764  grpid  12774  grpasscan1  12794  dfgrp3mlem  12829  dfgrp3me  12831  mulgnn0p1  12855  mulgaddcom  12867  mulginvcom  12868  mulgass  12880  mulgpropdg  12885  cmncom  12904  uniopn  13070  istopon  13082  fiinbas  13118  tg2  13131  tgcl  13135  0nnei  13224  tgrest  13240  tgcn  13279  cnpnei  13290  cncnp2m  13302  lmtopcnp  13321  tx2cn  13341  txcn  13346  cnmpt21  13362  isxmet2d  13419  metrest  13577  metcnpi3  13588  tgioo  13617  fsumcncntop  13627  elcncf1di  13637  climcncf  13642  cncfco  13649  suplociccreex  13673  cnplimcim  13707  cnlimci  13713  reeff1olem  13763  efltlemlt  13766  zabsle1  13971  lgslem3  13974  lgsmod  13998  lgsdir2lem5  14004  lgsdir2  14005  lgsne0  14010  lgsdirnn0  14019  bj-charfun  14119  bj-charfunr  14122  bj-charfunbi  14123  bj-prexg  14223  peano5set  14252  bj-peano4  14267  bj-nn0suc  14276  bj-nn0sucALT  14290  bj-findis  14291  exmidsbthrlem  14331  trilpolemres  14351  trirec0  14353  nconstwlpolem  14373  neapmkv  14376