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  342  pm3.34  343  pm3.35  344  pm5.31  345  imp4b  347  imp41  350  imp42  351  imp43  352  imp44  353  imp45  354  imp5g  357  expr  372  impac  378  sylan9  406  sylan9r  407  imdistani  441  mpan10  465  adantl4r  508  adantl5r  516  adantl6r  517  a2and  547  anabsi5  568  anim12dan  589  pm3.43  591  con3dimp  624  annimim  675  imnan  679  jaoian  784  jaodan  786  stdcndc  830  impidc  843  pm2.5gdc  851  con2bidc  860  pm5.18dc  868  dfandc  869  pm4.63dc  871  pm4.54dc  887  pm4.79dc  888  orcanai  913  annimdc  921  pm4.55dc  922  orandc  923  pm4.82  934  pm3.11dc  941  pm3.12dc  942  dn1dc  944  3jcad  1162  3expia  1183  3an1rs  1197  3imp1  1198  3imp2  1200  syl3anl2  1265  3jaoian  1283  3jaodan  1284  mp3anl1  1309  mp3anl2  1310  mp3anl3  1311  ecased  1327  xor3dc  1365  pm5.15dc  1367  xor2dc  1368  xornbidc  1369  xordc  1370  nbbndc  1372  biassdc  1373  bilukdc  1374  dfbi3dc  1375  pm5.24dc  1376  xordidc  1377  alanimi  1435  19.29  1599  equs4  1703  equsexd  1707  spimth  1713  equs5a  1766  ax11v2  1792  ax11b  1798  equs5or  1802  sb5rf  1824  equvin  1835  nfsb4t  1989  eu5  2046  mopick  2077  euexex  2084  2euswapdc  2090  exists2  2096  eqrdav  2138  dvelimdc  2301  nebidc  2388  pm13.18  2389  nelne1  2398  nelne2  2399  ralrimdvv  2516  r19.21bi  2520  r19.26  2558  ralbi  2564  rexbi  2565  r19.29  2569  vtoclgft  2736  rspcva  2787  rspc2va  2803  elabgt  2825  eqeu  2854  mob2  2864  mob  2866  euind  2871  reu6  2873  reuind  2889  sbctt  2975  rspsbca  2992  sbcnestgf  3051  rspcsbela  3059  ssel2  3092  sselda  3097  sstr  3105  nssne1  3155  nssne2  3156  reuss2  3356  reupick  3360  reupick2  3362  reximdva0m  3378  ssn0  3405  disjel  3417  ssdisj  3419  absneu  3595  preqr1g  3693  prel12  3698  dfiun2g  3845  nbrne1  3947  nbrne2  3948  mpteq12f  4008  triun  4039  csbexga  4056  iinexgm  4079  prexg  4133  copsex2t  4167  swopo  4228  poirr  4229  potr  4230  pofun  4234  issod  4241  ordelss  4301  trssord  4302  limelon  4321  trsuc  4344  eusvnfb  4375  rabxfrd  4390  regexmidlem1  4448  nordeq  4459  suc11g  4472  nnsuc  4529  brrelex12  4577  vtoclr  4587  optocl  4615  relop  4689  brcogw  4708  breldmg  4745  elreldm  4765  riinint  4800  issref  4921  xpidtr  4929  trin2  4930  cnveqb  4994  funopg  5157  funssres  5165  fununi  5191  funimass2  5201  imain  5205  fnun  5229  fco  5288  opelf  5294  f0rn0  5317  f1oun  5387  fun11iun  5388  fv3  5444  ndmfvg  5452  fvelima  5473  fvopab3ig  5495  fvmptssdm  5505  fvmptf  5513  fvimacnv  5535  fmptco  5586  funfvima2  5650  funfvima3  5651  f1veqaeq  5670  f1ocnvfvrneq  5683  fliftfun  5697  isotr  5717  isoini  5719  isopolem  5723  isosolem  5725  moriotass  5758  acexmidlem2  5771  suppssfv  5978  suppssov1  5979  f1dmex  6014  releldm2  6083  f1o2ndf1  6125  poxp  6129  tposf2  6165  iunon  6181  smoel2  6200  tfrlem9  6216  tfrexlem  6231  tfr1onlembxssdm  6240  tfr1onlemres  6246  tfrcllembxssdm  6253  tfrcllemres  6259  tfrcl  6261  tfri3  6264  frecabcl  6296  sucinc2  6342  nnacom  6380  nnmcom  6385  nnsucsssuc  6388  nnsucuniel  6391  nntri2or2  6394  nnaordi  6404  nnmordi  6412  nnaordex  6423  nnm00  6425  ectocld  6495  iinerm  6501  th3qlem2  6532  elpm2r  6560  mapsncnv  6589  mptelixpg  6628  ixpsnf1o  6630  f1oen3g  6648  f1oeng  6651  en2d  6662  en3d  6663  dom2lem  6666  fundmen  6700  fundmeng  6701  unen  6710  xpdom2  6725  xpdom2g  6726  fopwdom  6730  nneneq  6751  phpm  6759  phpelm  6760  dif1enen  6774  fin0  6779  findcard  6782  diffifi  6788  ac6sfi  6792  onunsnss  6805  fiintim  6817  xpfi  6818  fidcenum  6844  sbthlem1  6845  sbthlemi3  6847  sbthlemi10  6854  elfir  6861  isotilem  6893  inflbti  6911  ordiso2  6920  eldju2ndl  6957  eldju2ndr  6958  updjudhf  6964  mkvprop  7032  carden2bex  7045  pm54.43  7046  exmidfodomrlemeldju  7055  exmidfodomrlemreseldju  7056  exmidfodomrlemim  7057  ltmpig  7147  enq0sym  7240  addnq0mo  7255  mulnq0mo  7256  prarloclem3step  7304  prarloclem3  7305  genpml  7325  genpmu  7326  genprndl  7329  genprndu  7330  genpdisj  7331  distrlem1prl  7390  distrlem1pru  7391  distrlem4prl  7392  distrlem4pru  7393  distrlem5prl  7394  distrlem5pru  7395  ltsopr  7404  ltaddpr  7405  addcanprleml  7422  addcanprlemu  7423  recexprlemm  7432  recexprlemlol  7434  recexprlemupu  7436  aptiprleml  7447  aptiprlemu  7448  caucvgprlemnkj  7474  caucvgprlemnbj  7475  addsrmo  7551  mulsrmo  7552  srpospr  7591  caucvgsr  7610  axprecex  7688  mulgt0  7839  ltne  7849  cnegexlem1  7937  cnegexlem2  7938  negf1o  8144  addgt0  8210  addgegt0  8211  addgtge0  8212  addge0  8213  recexre  8340  mulge0  8381  recexap  8414  prodgt02  8611  prodge02  8613  ltmul12a  8618  mulgt1  8621  nndivtr  8762  addltmul  8956  elnnnn0b  9021  xnn0nnn0pnf  9053  elnnz  9064  zmulcl  9107  nn0n0n1ge2  9121  nn0lt2  9132  nn0le2is012  9133  uzind2  9163  nn0ind-raph  9168  eluzp1m1  9349  uz3m2nn  9368  supinfneg  9390  infsupneg  9391  negm  9407  lbzbi  9408  qaddcl  9427  qmulcl  9429  qreccl  9434  ledivge1le  9513  nn0ledivnn  9554  xrltne  9596  xrre  9603  xrre2  9604  xrre3  9605  ge0gtmnf  9606  xltnegi  9618  xnn0xadd0  9650  xnegdi  9651  xposdif  9665  xlesubadd  9666  iccsupr  9749  icoshft  9773  icoshftf1o  9774  fznlem  9821  fzen  9823  uzsubsubfz  9827  fzsuc2  9859  elfz1b  9870  elfz0ubfz0  9902  elfz0fzfz0  9903  fz0fzelfz0  9904  fz0fzdiffz0  9907  elfzmlbp  9909  difelfznle  9912  fzofzim  9965  eluzgtdifelfzo  9974  elfzodifsumelfzo  9978  elfzonlteqm1  9987  elfzom1p1elfzo  9991  ssfzo12bi  10002  subfzo0  10019  exbtwnzlemstep  10025  modqmuladdnn0  10141  modfzo0difsn  10168  addmodlteq  10171  frec2uzlt2d  10177  frecuzrdgtcl  10185  frecuzrdgfunlem  10192  m1expcl2  10315  expge1  10330  leexp2r  10347  expubnd  10350  zesq  10410  expnlbnd  10416  nn0opthd  10468  faclbnd  10487  bcpasc  10512  hashprg  10554  seq3coll  10585  rexanuz  10760  rexuz3  10762  r19.29uz  10764  r19.2uz  10765  absnid  10845  leabs  10846  ltabs  10859  icodiamlt  10952  maxleast  10985  negfi  10999  climcn2  11078  climcau  11116  climcaucn  11120  sumdc  11127  fsum3cvg  11147  isumz  11158  fsumf1o  11159  fisumss  11161  isumss2  11162  fsumzcl2  11174  fsumsplit  11176  fsumsplitsnun  11188  sumsplitdc  11201  fsum2dlemstep  11203  telfsumo  11235  fsumparts  11239  fsumiun  11246  isumrpcl  11263  fproddccvg  11341  efexp  11388  efieq1re  11478  dvds0lem  11503  dvds2ln  11526  dvdssub2  11535  dvdsadd2b  11540  dvdsabseq  11545  divconjdvds  11547  dvdsdivcl  11548  odd2np1  11570  oddge22np1  11578  opoe  11592  omoe  11593  opeo  11594  omeo  11595  m1expo  11597  nn0ehalf  11600  nn0o1gt2  11602  nno  11603  divalgb  11622  ndvdsadd  11628  zsupcllemex  11639  zssinfcl  11641  gcd0id  11667  gcdneg  11670  gcdaddm  11672  bezoutlemstep  11685  dfgcd2  11702  gcddiv  11707  dvdsmulgcd  11713  bezoutr  11720  bezoutr1  11721  algfx  11733  lcmgcdlem  11758  lcmgcdeq  11764  coprmdvds  11773  divgcdcoprmex  11783  cncongr1  11784  cncongr2  11785  isprm3  11799  dvdsnprmd  11806  prmgt1  11812  oddprmgt2  11814  isprm6  11825  cncongrprm  11835  phibndlem  11892  phimullem  11901  ennnfone  11938  unct  11954  uniopn  12168  istopon  12180  fiinbas  12216  tg2  12229  tgcl  12233  0nnei  12322  tgrest  12338  tgcn  12377  cnpnei  12388  cncnp2m  12400  lmtopcnp  12419  tx2cn  12439  txcn  12444  cnmpt21  12460  isxmet2d  12517  metrest  12675  metcnpi3  12686  tgioo  12715  fsumcncntop  12725  elcncf1di  12735  climcncf  12740  cncfco  12747  suplociccreex  12771  cnplimcim  12805  cnlimci  12811  bj-prexg  13109  peano5set  13138  bj-peano4  13153  bj-nn0suc  13162  bj-nn0sucALT  13176  bj-findis  13177  exmidsbthrlem  13217  trilpolemres  13235