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  636  annimim  687  imnan  691  jaoian  796  jaodan  798  stdcndc  846  impidc  859  pm2.5gdc  867  con2bidc  876  pm5.18dc  884  dfandc  885  pm4.63dc  887  pm4.54dc  903  pm4.79dc  904  orcanai  929  annimdc  939  pm4.55dc  940  orandc  941  pm4.82  952  pm3.11dc  959  pm3.12dc  960  dn1dc  962  3jcad  1180  3expia  1207  3an1rs  1221  3imp1  1222  3imp2  1224  syl3anl2  1298  3jaoian  1316  3jaodan  1317  mp3anl1  1342  mp3anl2  1343  mp3anl3  1344  ecased  1360  xor3dc  1398  pm5.15dc  1400  xor2dc  1401  xornbidc  1402  xordc  1403  nbbndc  1405  biassdc  1406  bilukdc  1407  dfbi3dc  1408  pm5.24dc  1409  xordidc  1410  alanimi  1473  19.29  1634  equs4  1739  equsexd  1743  spimth  1749  equs5a  1808  ax11v2  1834  ax11b  1840  equs5or  1844  sb5rf  1866  equvin  1877  nfsb4t  2033  eu5  2092  mopick  2123  euexex  2130  2euswapdc  2136  exists2  2142  eqrdav  2195  dvelimdc  2360  nebidc  2447  pm13.18  2448  nelne1  2457  nelne2  2458  rspa  2545  ralrimdvv  2581  r19.21bi  2585  r19.26  2623  ralbi  2629  rexbi  2630  r19.29  2634  vtoclgft  2814  rspcva  2866  rspc2va  2882  elabgt  2905  eqeu  2934  mob2  2944  mob  2946  euind  2951  reu6  2953  reuind  2969  sbctt  3056  rspsbca  3073  sbcnestgf  3136  rspcsbela  3144  ssel2  3178  sselda  3183  sstr  3191  nssne1  3241  nssne2  3242  reuss2  3443  reupick  3447  reupick2  3449  reximdva0m  3466  ssn0  3493  disjel  3505  ssdisj  3507  absneu  3694  preqr1g  3796  prel12  3801  dfiun2g  3948  nbrne1  4052  nbrne2  4053  mpteq12f  4113  triun  4144  csbexga  4161  iinexgm  4187  prexg  4244  copsex2t  4278  swopo  4341  poirr  4342  potr  4343  pofun  4347  issod  4354  ordelss  4414  trssord  4415  limelon  4434  trsuc  4457  eusvnfb  4489  rabxfrd  4504  regexmidlem1  4569  nordeq  4580  suc11g  4593  nnsuc  4652  brrelex12  4701  vtoclr  4711  optocl  4739  relop  4816  brcogw  4835  breldmg  4872  elreldm  4892  riinint  4927  issref  5052  xpidtr  5060  trin2  5061  cnveqb  5125  funopg  5292  funssres  5300  fununi  5326  funimass2  5336  imain  5340  fnun  5364  fco  5423  opelf  5429  f0rn0  5452  f1oun  5524  fun11iun  5525  fv3  5581  ndmfvg  5589  fvelima  5612  fvopab3ig  5635  fvmptssdm  5646  fvmptf  5654  fvimacnv  5677  fmptco  5728  funfvima2  5795  funfvima3  5796  f1veqaeq  5816  f1ocnvfvrneq  5829  fliftfun  5843  isotr  5863  isoini  5865  isopolem  5869  isosolem  5871  moriotass  5906  acexmidlem2  5919  suppssfv  6131  suppssov1  6132  f1dmex  6173  releldm2  6243  f1o2ndf1  6286  poxp  6290  tposf2  6326  iunon  6342  smoel2  6361  tfrlem9  6377  tfrexlem  6392  tfr1onlembxssdm  6401  tfr1onlemres  6407  tfrcllembxssdm  6414  tfrcllemres  6420  tfrcl  6422  tfri3  6425  frecabcl  6457  sucinc2  6504  nnacom  6542  nnmcom  6547  nnsucsssuc  6550  nnsucuniel  6553  nntri2or2  6556  nnaordi  6566  nnmordi  6574  nnaordex  6586  nnm00  6588  ectocld  6660  iinerm  6666  th3qlem2  6697  elpm2r  6725  mapsncnv  6754  mptelixpg  6793  ixpsnf1o  6795  f1oen3g  6813  f1oeng  6816  en2d  6827  en3d  6828  dom2lem  6831  fundmen  6865  fundmeng  6866  unen  6875  xpdom2  6890  xpdom2g  6891  fopwdom  6897  nneneq  6918  phpm  6926  phpelm  6927  dif1enen  6941  fin0  6946  findcard  6949  diffifi  6955  ac6sfi  6959  onunsnss  6978  fiintim  6992  xpfi  6993  infidc  7000  fidcenum  7022  sbthlem1  7023  sbthlemi3  7025  sbthlemi10  7032  elfir  7039  isotilem  7072  inflbti  7090  ordiso2  7101  eldju2ndl  7138  eldju2ndr  7139  updjudhf  7145  mkvprop  7224  carden2bex  7256  pm54.43  7257  exmidfodomrlemeldju  7266  exmidfodomrlemreseldju  7267  exmidfodomrlemim  7268  ltmpig  7406  enq0sym  7499  addnq0mo  7514  mulnq0mo  7515  prarloclem3step  7563  prarloclem3  7564  genpml  7584  genpmu  7585  genprndl  7588  genprndu  7589  genpdisj  7590  distrlem1prl  7649  distrlem1pru  7650  distrlem4prl  7651  distrlem4pru  7652  distrlem5prl  7653  distrlem5pru  7654  ltsopr  7663  ltaddpr  7664  addcanprleml  7681  addcanprlemu  7682  recexprlemm  7691  recexprlemlol  7693  recexprlemupu  7695  aptiprleml  7706  aptiprlemu  7707  caucvgprlemnkj  7733  caucvgprlemnbj  7734  addsrmo  7810  mulsrmo  7811  srpospr  7850  caucvgsr  7869  axprecex  7947  mpomulf  8016  mulgt0  8101  ltne  8111  cnegexlem1  8201  cnegexlem2  8202  negf1o  8408  addgt0  8475  addgegt0  8476  addgtge0  8477  addge0  8478  recexre  8605  mulge0  8646  recexap  8680  prodgt02  8880  prodge02  8882  ltmul12a  8887  mulgt1  8890  nndivtr  9032  addltmul  9228  elnnnn0b  9293  xnn0nnn0pnf  9325  elnnz  9336  zmulcl  9379  nn0n0n1ge2  9396  nn0lt2  9407  nn0le2is012  9408  uzind2  9438  nn0ind-raph  9443  eluzp1m1  9625  uz3m2nn  9647  supinfneg  9669  infsupneg  9670  infregelbex  9672  negm  9689  lbzbi  9690  qaddcl  9709  qmulcl  9711  qreccl  9716  elpq  9723  ledivge1le  9801  nn0ledivnn  9842  xrltne  9888  xrre  9895  xrre2  9896  xrre3  9897  ge0gtmnf  9898  xltnegi  9910  xnn0xadd0  9942  xnegdi  9943  xposdif  9957  xlesubadd  9958  iccsupr  10041  icoshft  10065  icoshftf1o  10066  fznlem  10116  fzen  10118  uzsubsubfz  10122  fzsuc2  10154  elfz1b  10165  elfz0ubfz0  10200  elfz0fzfz0  10201  fz0fzelfz0  10202  fz0fzdiffz0  10205  elfzmlbp  10207  difelfznle  10210  fzofzim  10264  eluzgtdifelfzo  10273  elfzodifsumelfzo  10277  elfzonlteqm1  10286  elfzom1p1elfzo  10290  ssfzo12bi  10301  subfzo0  10318  zsupcllemex  10320  zssinfcl  10322  exbtwnzlemstep  10337  modqmuladdnn0  10460  modfzo0difsn  10487  addmodlteq  10490  frec2uzlt2d  10496  frecuzrdgtcl  10504  frecuzrdgfunlem  10511  seqf1og  10613  m1expcl2  10653  expge1  10668  leexp2r  10685  expubnd  10688  zesq  10750  expnlbnd  10756  nn0ltexp2  10801  nn0opthd  10814  faclbnd  10833  bcpasc  10858  hashprg  10900  seq3coll  10934  wrdnval  10965  wrdsymb0  10967  fstwrdne  10973  wrdred1hash  10978  rexanuz  11153  rexuz3  11155  r19.29uz  11157  r19.2uz  11158  absnid  11238  leabs  11239  ltabs  11252  icodiamlt  11345  maxleast  11378  negfi  11393  climcn2  11474  climcau  11512  climcaucn  11516  sumdc  11523  fsum3cvg  11543  isumz  11554  fsumf1o  11555  fisumss  11557  isumss2  11558  fsumzcl2  11570  fsumsplit  11572  fsumsplitsnun  11584  sumsplitdc  11597  fsum2dlemstep  11599  telfsumo  11631  fsumparts  11635  fsumiun  11642  isumrpcl  11659  fproddccvg  11737  prod1dc  11751  prodssdc  11754  fprodssdc  11755  prodsnf  11757  fprodsplitdc  11761  fprod2dlemstep  11787  fprodmodd  11806  efexp  11847  efieq1re  11937  p1modz1  11959  dvds0lem  11966  dvds2ln  11989  dvdssub2  12000  dvdsadd2b  12005  dvdsabseq  12012  divconjdvds  12014  dvdsdivcl  12015  odd2np1  12038  oddge22np1  12046  opoe  12060  omoe  12061  opeo  12062  omeo  12063  m1expo  12065  nn0ehalf  12068  nn0o1gt2  12070  nno  12071  divalgb  12090  ndvdsadd  12096  gcd0id  12146  gcdneg  12149  gcdaddm  12151  bezoutlemstep  12164  dfgcd2  12181  gcddiv  12186  dvdsmulgcd  12192  bezoutr  12199  bezoutr1  12200  uzwodc  12204  nninfctlemfo  12207  algfx  12220  lcmgcdlem  12245  lcmgcdeq  12251  coprmdvds  12260  divgcdcoprmex  12270  cncongr1  12271  cncongr2  12272  isprm3  12286  dvdsnprmd  12293  prmgt1  12300  oddprmgt2  12302  isprm6  12315  cncongrprm  12325  phibndlem  12384  phimullem  12393  powm2modprm  12421  modprm0  12423  modprmn0modprm0  12425  prm23lt5  12432  pcneg  12494  pcprmpw2  12502  dvdsprmpweqnn  12505  dvdsprmpweqle  12506  pcaddlem  12508  fldivp1  12517  pcfac  12519  oddprmdvds  12523  prmunb  12531  ennnfone  12642  unct  12659  lidrididd  13025  gsummgmpropd  13037  sgrpass  13051  issgrpd  13055  issubmnd  13083  mnd1id  13088  insubm  13117  dfgrp2  13159  grpid  13171  grpasscan1  13195  dfgrp3mlem  13230  dfgrp3me  13232  imasgrp2  13240  mulgnn0gsum  13258  mulgnn0p1  13263  mulgaddcom  13276  mulginvcom  13277  mulgass  13289  mulgpropdg  13294  subginv  13311  issubg2m  13319  issubg4m  13323  grpissubg  13324  resgrpisgrp  13325  subgintm  13328  kerf1ghm  13404  cmncom  13432  imasabl  13466  rngdi  13496  rngdir  13497  rngpropd  13511  imasrng  13512  imasring  13620  nzrunit  13744  issubrng2  13766  subrngintm  13768  issubrg2  13797  subrgintm  13799  lmodfopnelem1  13880  lmodfopnelem2  13881  lmodfopne  13882  islssm  13913  islidlm  14035  rnglidlmcl  14036  dflidl2rng  14037  rnglidlmmgm  14052  rnglidlmsgrp  14053  rnglidlrng  14054  dvdsrzring  14159  znidom  14213  uniopn  14237  istopon  14249  fiinbas  14285  tg2  14296  tgcl  14300  0nnei  14389  tgrest  14405  tgcn  14444  cnpnei  14455  cncnp2m  14467  lmtopcnp  14486  tx2cn  14506  txcn  14511  cnmpt21  14527  isxmet2d  14584  metrest  14742  metcnpi3  14753  tgioo  14790  fsumcncntop  14803  elcncf1di  14815  climcncf  14820  cncfco  14827  suplociccreex  14860  cnplimcim  14903  cnlimci  14909  reeff1olem  15007  efltlemlt  15010  zabsle1  15240  lgslem3  15243  lgsmod  15267  lgsdir2lem5  15273  lgsdir2  15274  lgsne0  15279  lgsdirnn0  15288  gausslemma2dlem0f  15295  gausslemma2dlem1a  15299  gausslemma2dlem3  15304  2lgslem1c  15331  2lgslem3a1  15338  2lgslem3b1  15339  2lgslem3c1  15340  2lgslem3d1  15341  2lgslem3  15342  2lgsoddprmlem2  15347  bj-charfun  15453  bj-charfunr  15456  bj-charfunbi  15457  bj-prexg  15557  peano5set  15586  bj-peano4  15601  bj-nn0suc  15610  bj-nn0sucALT  15624  bj-findis  15625  exmidsbthrlem  15666  trilpolemres  15686  trirec0  15688  nconstwlpolem  15709  neapmkv  15712