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  1459  19.29  1620  equs4  1725  equsexd  1729  spimth  1735  equs5a  1794  ax11v2  1820  ax11b  1826  equs5or  1830  sb5rf  1852  equvin  1863  nfsb4t  2014  eu5  2073  mopick  2104  euexex  2111  2euswapdc  2117  exists2  2123  eqrdav  2176  dvelimdc  2340  nebidc  2427  pm13.18  2428  nelne1  2437  nelne2  2438  rspa  2525  ralrimdvv  2561  r19.21bi  2565  r19.26  2603  ralbi  2609  rexbi  2610  r19.29  2614  vtoclgft  2788  rspcva  2840  rspc2va  2856  elabgt  2879  eqeu  2908  mob2  2918  mob  2920  euind  2925  reu6  2927  reuind  2943  sbctt  3030  rspsbca  3047  sbcnestgf  3109  rspcsbela  3117  ssel2  3151  sselda  3156  sstr  3164  nssne1  3214  nssne2  3215  reuss2  3416  reupick  3420  reupick2  3422  reximdva0m  3439  ssn0  3466  disjel  3478  ssdisj  3480  absneu  3665  preqr1g  3767  prel12  3772  dfiun2g  3919  nbrne1  4023  nbrne2  4024  mpteq12f  4084  triun  4115  csbexga  4132  iinexgm  4155  prexg  4212  copsex2t  4246  swopo  4307  poirr  4308  potr  4309  pofun  4313  issod  4320  ordelss  4380  trssord  4381  limelon  4400  trsuc  4423  eusvnfb  4455  rabxfrd  4470  regexmidlem1  4533  nordeq  4544  suc11g  4557  nnsuc  4616  brrelex12  4665  vtoclr  4675  optocl  4703  relop  4778  brcogw  4797  breldmg  4834  elreldm  4854  riinint  4889  issref  5012  xpidtr  5020  trin2  5021  cnveqb  5085  funopg  5251  funssres  5259  fununi  5285  funimass2  5295  imain  5299  fnun  5323  fco  5382  opelf  5388  f0rn0  5411  f1oun  5482  fun11iun  5483  fv3  5539  ndmfvg  5547  fvelima  5568  fvopab3ig  5591  fvmptssdm  5601  fvmptf  5609  fvimacnv  5632  fmptco  5683  funfvima2  5750  funfvima3  5751  f1veqaeq  5770  f1ocnvfvrneq  5783  fliftfun  5797  isotr  5817  isoini  5819  isopolem  5823  isosolem  5825  moriotass  5859  acexmidlem2  5872  suppssfv  6079  suppssov1  6080  f1dmex  6117  releldm2  6186  f1o2ndf1  6229  poxp  6233  tposf2  6269  iunon  6285  smoel2  6304  tfrlem9  6320  tfrexlem  6335  tfr1onlembxssdm  6344  tfr1onlemres  6350  tfrcllembxssdm  6357  tfrcllemres  6363  tfrcl  6365  tfri3  6368  frecabcl  6400  sucinc2  6447  nnacom  6485  nnmcom  6490  nnsucsssuc  6493  nnsucuniel  6496  nntri2or2  6499  nnaordi  6509  nnmordi  6517  nnaordex  6529  nnm00  6531  ectocld  6601  iinerm  6607  th3qlem2  6638  elpm2r  6666  mapsncnv  6695  mptelixpg  6734  ixpsnf1o  6736  f1oen3g  6754  f1oeng  6757  en2d  6768  en3d  6769  dom2lem  6772  fundmen  6806  fundmeng  6807  unen  6816  xpdom2  6831  xpdom2g  6832  fopwdom  6836  nneneq  6857  phpm  6865  phpelm  6866  dif1enen  6880  fin0  6885  findcard  6888  diffifi  6894  ac6sfi  6898  onunsnss  6916  fiintim  6928  xpfi  6929  fidcenum  6955  sbthlem1  6956  sbthlemi3  6958  sbthlemi10  6965  elfir  6972  isotilem  7005  inflbti  7023  ordiso2  7034  eldju2ndl  7071  eldju2ndr  7072  updjudhf  7078  mkvprop  7156  carden2bex  7188  pm54.43  7189  exmidfodomrlemeldju  7198  exmidfodomrlemreseldju  7199  exmidfodomrlemim  7200  ltmpig  7338  enq0sym  7431  addnq0mo  7446  mulnq0mo  7447  prarloclem3step  7495  prarloclem3  7496  genpml  7516  genpmu  7517  genprndl  7520  genprndu  7521  genpdisj  7522  distrlem1prl  7581  distrlem1pru  7582  distrlem4prl  7583  distrlem4pru  7584  distrlem5prl  7585  distrlem5pru  7586  ltsopr  7595  ltaddpr  7596  addcanprleml  7613  addcanprlemu  7614  recexprlemm  7623  recexprlemlol  7625  recexprlemupu  7627  aptiprleml  7638  aptiprlemu  7639  caucvgprlemnkj  7665  caucvgprlemnbj  7666  addsrmo  7742  mulsrmo  7743  srpospr  7782  caucvgsr  7801  axprecex  7879  mulgt0  8032  ltne  8042  cnegexlem1  8132  cnegexlem2  8133  negf1o  8339  addgt0  8405  addgegt0  8406  addgtge0  8407  addge0  8408  recexre  8535  mulge0  8576  recexap  8610  prodgt02  8810  prodge02  8812  ltmul12a  8817  mulgt1  8820  nndivtr  8961  addltmul  9155  elnnnn0b  9220  xnn0nnn0pnf  9252  elnnz  9263  zmulcl  9306  nn0n0n1ge2  9323  nn0lt2  9334  nn0le2is012  9335  uzind2  9365  nn0ind-raph  9370  eluzp1m1  9551  uz3m2nn  9573  supinfneg  9595  infsupneg  9596  infregelbex  9598  negm  9615  lbzbi  9616  qaddcl  9635  qmulcl  9637  qreccl  9642  elpq  9648  ledivge1le  9726  nn0ledivnn  9767  xrltne  9813  xrre  9820  xrre2  9821  xrre3  9822  ge0gtmnf  9823  xltnegi  9835  xnn0xadd0  9867  xnegdi  9868  xposdif  9882  xlesubadd  9883  iccsupr  9966  icoshft  9990  icoshftf1o  9991  fznlem  10041  fzen  10043  uzsubsubfz  10047  fzsuc2  10079  elfz1b  10090  elfz0ubfz0  10125  elfz0fzfz0  10126  fz0fzelfz0  10127  fz0fzdiffz0  10130  elfzmlbp  10132  difelfznle  10135  fzofzim  10188  eluzgtdifelfzo  10197  elfzodifsumelfzo  10201  elfzonlteqm1  10210  elfzom1p1elfzo  10214  ssfzo12bi  10225  subfzo0  10242  exbtwnzlemstep  10248  modqmuladdnn0  10368  modfzo0difsn  10395  addmodlteq  10398  frec2uzlt2d  10404  frecuzrdgtcl  10412  frecuzrdgfunlem  10419  m1expcl2  10542  expge1  10557  leexp2r  10574  expubnd  10577  zesq  10639  expnlbnd  10645  nn0ltexp2  10689  nn0opthd  10702  faclbnd  10721  bcpasc  10746  hashprg  10788  seq3coll  10822  rexanuz  10997  rexuz3  10999  r19.29uz  11001  r19.2uz  11002  absnid  11082  leabs  11083  ltabs  11096  icodiamlt  11189  maxleast  11222  negfi  11236  climcn2  11317  climcau  11355  climcaucn  11359  sumdc  11366  fsum3cvg  11386  isumz  11397  fsumf1o  11398  fisumss  11400  isumss2  11401  fsumzcl2  11413  fsumsplit  11415  fsumsplitsnun  11427  sumsplitdc  11440  fsum2dlemstep  11442  telfsumo  11474  fsumparts  11478  fsumiun  11485  isumrpcl  11502  fproddccvg  11580  prod1dc  11594  prodssdc  11597  fprodssdc  11598  prodsnf  11600  fprodsplitdc  11604  fprod2dlemstep  11630  fprodmodd  11649  efexp  11690  efieq1re  11779  p1modz1  11801  dvds0lem  11808  dvds2ln  11831  dvdssub2  11842  dvdsadd2b  11847  dvdsabseq  11853  divconjdvds  11855  dvdsdivcl  11856  odd2np1  11878  oddge22np1  11886  opoe  11900  omoe  11901  opeo  11902  omeo  11903  m1expo  11905  nn0ehalf  11908  nn0o1gt2  11910  nno  11911  divalgb  11930  ndvdsadd  11936  zsupcllemex  11947  zssinfcl  11949  gcd0id  11980  gcdneg  11983  gcdaddm  11985  bezoutlemstep  11998  dfgcd2  12015  gcddiv  12020  dvdsmulgcd  12026  bezoutr  12033  bezoutr1  12034  uzwodc  12038  algfx  12052  lcmgcdlem  12077  lcmgcdeq  12083  coprmdvds  12092  divgcdcoprmex  12102  cncongr1  12103  cncongr2  12104  isprm3  12118  dvdsnprmd  12125  prmgt1  12132  oddprmgt2  12134  isprm6  12147  cncongrprm  12157  phibndlem  12216  phimullem  12225  powm2modprm  12252  modprm0  12254  modprmn0modprm0  12256  prm23lt5  12263  pcneg  12324  pcprmpw2  12332  dvdsprmpweqnn  12335  dvdsprmpweqle  12336  pcaddlem  12338  fldivp1  12346  pcfac  12348  oddprmdvds  12352  prmunb  12360  ennnfone  12426  unct  12443  lidrididd  12801  sgrpass  12814  issubmnd  12843  mnd1id  12848  insubm  12872  dfgrp2  12902  grpid  12912  grpasscan1  12933  dfgrp3mlem  12968  dfgrp3me  12970  mulgnn0p1  12994  mulgaddcom  13007  mulginvcom  13008  mulgass  13020  mulgpropdg  13025  subginv  13041  issubg2m  13049  issubg4m  13053  grpissubg  13054  resgrpisgrp  13055  subgintm  13058  cmncom  13105  nzrunit  13329  issubrg2  13362  subrgintm  13364  lmodfopnelem1  13414  lmodfopnelem2  13415  lmodfopne  13416  dvdsrzring  13496  uniopn  13504  istopon  13516  fiinbas  13552  tg2  13563  tgcl  13567  0nnei  13656  tgrest  13672  tgcn  13711  cnpnei  13722  cncnp2m  13734  lmtopcnp  13753  tx2cn  13773  txcn  13778  cnmpt21  13794  isxmet2d  13851  metrest  14009  metcnpi3  14020  tgioo  14049  fsumcncntop  14059  elcncf1di  14069  climcncf  14074  cncfco  14081  suplociccreex  14105  cnplimcim  14139  cnlimci  14145  reeff1olem  14195  efltlemlt  14198  zabsle1  14403  lgslem3  14406  lgsmod  14430  lgsdir2lem5  14436  lgsdir2  14437  lgsne0  14442  lgsdirnn0  14451  2lgsoddprmlem2  14457  bj-charfun  14562  bj-charfunr  14565  bj-charfunbi  14566  bj-prexg  14666  peano5set  14695  bj-peano4  14710  bj-nn0suc  14719  bj-nn0sucALT  14733  bj-findis  14734  exmidsbthrlem  14773  trilpolemres  14793  trirec0  14795  nconstwlpolem  14815  neapmkv  14818