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  831  impidc  844  pm2.5gdc  852  con2bidc  861  pm5.18dc  869  dfandc  870  pm4.63dc  872  pm4.54dc  888  pm4.79dc  889  orcanai  914  annimdc  922  pm4.55dc  923  orandc  924  pm4.82  935  pm3.11dc  942  pm3.12dc  943  dn1dc  945  3jcad  1163  3expia  1184  3an1rs  1198  3imp1  1199  3imp2  1201  syl3anl2  1266  3jaoian  1284  3jaodan  1285  mp3anl1  1310  mp3anl2  1311  mp3anl3  1312  ecased  1328  xor3dc  1366  pm5.15dc  1368  xor2dc  1369  xornbidc  1370  xordc  1371  nbbndc  1373  biassdc  1374  bilukdc  1375  dfbi3dc  1376  pm5.24dc  1377  xordidc  1378  alanimi  1436  19.29  1600  equs4  1704  equsexd  1708  spimth  1714  equs5a  1767  ax11v2  1793  ax11b  1799  equs5or  1803  sb5rf  1825  equvin  1836  nfsb4t  1990  eu5  2047  mopick  2078  euexex  2085  2euswapdc  2091  exists2  2097  eqrdav  2139  dvelimdc  2302  nebidc  2389  pm13.18  2390  nelne1  2399  nelne2  2400  ralrimdvv  2519  r19.21bi  2523  r19.26  2561  ralbi  2567  rexbi  2568  r19.29  2572  vtoclgft  2739  rspcva  2791  rspc2va  2807  elabgt  2829  eqeu  2858  mob2  2868  mob  2870  euind  2875  reu6  2877  reuind  2893  sbctt  2979  rspsbca  2996  sbcnestgf  3056  rspcsbela  3064  ssel2  3097  sselda  3102  sstr  3110  nssne1  3160  nssne2  3161  reuss2  3361  reupick  3365  reupick2  3367  reximdva0m  3383  ssn0  3410  disjel  3422  ssdisj  3424  absneu  3603  preqr1g  3701  prel12  3706  dfiun2g  3853  nbrne1  3955  nbrne2  3956  mpteq12f  4016  triun  4047  csbexga  4064  iinexgm  4087  prexg  4141  copsex2t  4175  swopo  4236  poirr  4237  potr  4238  pofun  4242  issod  4249  ordelss  4309  trssord  4310  limelon  4329  trsuc  4352  eusvnfb  4383  rabxfrd  4398  regexmidlem1  4456  nordeq  4467  suc11g  4480  nnsuc  4537  brrelex12  4585  vtoclr  4595  optocl  4623  relop  4697  brcogw  4716  breldmg  4753  elreldm  4773  riinint  4808  issref  4929  xpidtr  4937  trin2  4938  cnveqb  5002  funopg  5165  funssres  5173  fununi  5199  funimass2  5209  imain  5213  fnun  5237  fco  5296  opelf  5302  f0rn0  5325  f1oun  5395  fun11iun  5396  fv3  5452  ndmfvg  5460  fvelima  5481  fvopab3ig  5503  fvmptssdm  5513  fvmptf  5521  fvimacnv  5543  fmptco  5594  funfvima2  5658  funfvima3  5659  f1veqaeq  5678  f1ocnvfvrneq  5691  fliftfun  5705  isotr  5725  isoini  5727  isopolem  5731  isosolem  5733  moriotass  5766  acexmidlem2  5779  suppssfv  5986  suppssov1  5987  f1dmex  6022  releldm2  6091  f1o2ndf1  6133  poxp  6137  tposf2  6173  iunon  6189  smoel2  6208  tfrlem9  6224  tfrexlem  6239  tfr1onlembxssdm  6248  tfr1onlemres  6254  tfrcllembxssdm  6261  tfrcllemres  6267  tfrcl  6269  tfri3  6272  frecabcl  6304  sucinc2  6350  nnacom  6388  nnmcom  6393  nnsucsssuc  6396  nnsucuniel  6399  nntri2or2  6402  nnaordi  6412  nnmordi  6420  nnaordex  6431  nnm00  6433  ectocld  6503  iinerm  6509  th3qlem2  6540  elpm2r  6568  mapsncnv  6597  mptelixpg  6636  ixpsnf1o  6638  f1oen3g  6656  f1oeng  6659  en2d  6670  en3d  6671  dom2lem  6674  fundmen  6708  fundmeng  6709  unen  6718  xpdom2  6733  xpdom2g  6734  fopwdom  6738  nneneq  6759  phpm  6767  phpelm  6768  dif1enen  6782  fin0  6787  findcard  6790  diffifi  6796  ac6sfi  6800  onunsnss  6813  fiintim  6825  xpfi  6826  fidcenum  6852  sbthlem1  6853  sbthlemi3  6855  sbthlemi10  6862  elfir  6869  isotilem  6901  inflbti  6919  ordiso2  6928  eldju2ndl  6965  eldju2ndr  6966  updjudhf  6972  mkvprop  7040  carden2bex  7062  pm54.43  7063  exmidfodomrlemeldju  7072  exmidfodomrlemreseldju  7073  exmidfodomrlemim  7074  ltmpig  7171  enq0sym  7264  addnq0mo  7279  mulnq0mo  7280  prarloclem3step  7328  prarloclem3  7329  genpml  7349  genpmu  7350  genprndl  7353  genprndu  7354  genpdisj  7355  distrlem1prl  7414  distrlem1pru  7415  distrlem4prl  7416  distrlem4pru  7417  distrlem5prl  7418  distrlem5pru  7419  ltsopr  7428  ltaddpr  7429  addcanprleml  7446  addcanprlemu  7447  recexprlemm  7456  recexprlemlol  7458  recexprlemupu  7460  aptiprleml  7471  aptiprlemu  7472  caucvgprlemnkj  7498  caucvgprlemnbj  7499  addsrmo  7575  mulsrmo  7576  srpospr  7615  caucvgsr  7634  axprecex  7712  mulgt0  7863  ltne  7873  cnegexlem1  7961  cnegexlem2  7962  negf1o  8168  addgt0  8234  addgegt0  8235  addgtge0  8236  addge0  8237  recexre  8364  mulge0  8405  recexap  8438  prodgt02  8635  prodge02  8637  ltmul12a  8642  mulgt1  8645  nndivtr  8786  addltmul  8980  elnnnn0b  9045  xnn0nnn0pnf  9077  elnnz  9088  zmulcl  9131  nn0n0n1ge2  9145  nn0lt2  9156  nn0le2is012  9157  uzind2  9187  nn0ind-raph  9192  eluzp1m1  9373  uz3m2nn  9395  supinfneg  9417  infsupneg  9418  negm  9434  lbzbi  9435  qaddcl  9454  qmulcl  9456  qreccl  9461  elpq  9467  ledivge1le  9543  nn0ledivnn  9584  xrltne  9626  xrre  9633  xrre2  9634  xrre3  9635  ge0gtmnf  9636  xltnegi  9648  xnn0xadd0  9680  xnegdi  9681  xposdif  9695  xlesubadd  9696  iccsupr  9779  icoshft  9803  icoshftf1o  9804  fznlem  9852  fzen  9854  uzsubsubfz  9858  fzsuc2  9890  elfz1b  9901  elfz0ubfz0  9933  elfz0fzfz0  9934  fz0fzelfz0  9935  fz0fzdiffz0  9938  elfzmlbp  9940  difelfznle  9943  fzofzim  9996  eluzgtdifelfzo  10005  elfzodifsumelfzo  10009  elfzonlteqm1  10018  elfzom1p1elfzo  10022  ssfzo12bi  10033  subfzo0  10050  exbtwnzlemstep  10056  modqmuladdnn0  10172  modfzo0difsn  10199  addmodlteq  10202  frec2uzlt2d  10208  frecuzrdgtcl  10216  frecuzrdgfunlem  10223  m1expcl2  10346  expge1  10361  leexp2r  10378  expubnd  10381  zesq  10441  expnlbnd  10447  nn0opthd  10500  faclbnd  10519  bcpasc  10544  hashprg  10586  seq3coll  10617  rexanuz  10792  rexuz3  10794  r19.29uz  10796  r19.2uz  10797  absnid  10877  leabs  10878  ltabs  10891  icodiamlt  10984  maxleast  11017  negfi  11031  climcn2  11110  climcau  11148  climcaucn  11152  sumdc  11159  fsum3cvg  11179  isumz  11190  fsumf1o  11191  fisumss  11193  isumss2  11194  fsumzcl2  11206  fsumsplit  11208  fsumsplitsnun  11220  sumsplitdc  11233  fsum2dlemstep  11235  telfsumo  11267  fsumparts  11271  fsumiun  11278  isumrpcl  11295  fproddccvg  11373  efexp  11425  efieq1re  11514  dvds0lem  11539  dvds2ln  11562  dvdssub2  11571  dvdsadd2b  11576  dvdsabseq  11581  divconjdvds  11583  dvdsdivcl  11584  odd2np1  11606  oddge22np1  11614  opoe  11628  omoe  11629  opeo  11630  omeo  11631  m1expo  11633  nn0ehalf  11636  nn0o1gt2  11638  nno  11639  divalgb  11658  ndvdsadd  11664  zsupcllemex  11675  zssinfcl  11677  gcd0id  11703  gcdneg  11706  gcdaddm  11708  bezoutlemstep  11721  dfgcd2  11738  gcddiv  11743  dvdsmulgcd  11749  bezoutr  11756  bezoutr1  11757  algfx  11769  lcmgcdlem  11794  lcmgcdeq  11800  coprmdvds  11809  divgcdcoprmex  11819  cncongr1  11820  cncongr2  11821  isprm3  11835  dvdsnprmd  11842  prmgt1  11848  oddprmgt2  11850  isprm6  11861  cncongrprm  11871  phibndlem  11928  phimullem  11937  ennnfone  11974  unct  11991  uniopn  12207  istopon  12219  fiinbas  12255  tg2  12268  tgcl  12272  0nnei  12361  tgrest  12377  tgcn  12416  cnpnei  12427  cncnp2m  12439  lmtopcnp  12458  tx2cn  12478  txcn  12483  cnmpt21  12499  isxmet2d  12556  metrest  12714  metcnpi3  12725  tgioo  12754  fsumcncntop  12764  elcncf1di  12774  climcncf  12779  cncfco  12786  suplociccreex  12810  cnplimcim  12844  cnlimci  12850  reeff1olem  12900  efltlemlt  12903  bj-prexg  13280  peano5set  13309  bj-peano4  13324  bj-nn0suc  13333  bj-nn0sucALT  13347  bj-findis  13348  exmidsbthrlem  13392  trilpolemres  13410  trirec0  13412  neapmkv  13425