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  688  imnan  692  jaoian  797  jaodan  799  stdcndc  847  impidc  860  pm2.5gdc  868  con2bidc  877  pm5.18dc  885  dfandc  886  pm4.63dc  888  pm4.54dc  904  pm4.79dc  905  orcanai  930  annimdc  940  pm4.55dc  941  orandc  942  pm4.82  953  pm3.11dc  960  pm3.12dc  961  dn1dc  963  3jcad  1181  3expia  1208  3an1rs  1222  3imp1  1223  3imp2  1225  syl3anl2  1299  3jaoian  1318  3jaodan  1319  mp3anl1  1344  mp3anl2  1345  mp3anl3  1346  ecased  1362  xor3dc  1407  pm5.15dc  1409  xor2dc  1410  xornbidc  1411  xordc  1412  nbbndc  1414  biassdc  1415  bilukdc  1416  dfbi3dc  1417  pm5.24dc  1418  xordidc  1419  alanimi  1482  19.29  1643  equs4  1748  equsexd  1752  spimth  1758  equs5a  1817  ax11v2  1843  ax11b  1849  equs5or  1853  sb5rf  1875  equvin  1886  nfsb4t  2042  eu5  2101  mopick  2132  euexex  2139  2euswapdc  2145  exists2  2151  eqrdav  2204  dvelimdc  2369  nebidc  2456  pm13.18  2457  nelne1  2466  nelne2  2467  rspa  2554  ralrimdvv  2590  r19.21bi  2594  r19.26  2632  ralbi  2638  rexbi  2639  r19.29  2643  vtoclgft  2823  rspcva  2875  rspc2va  2891  elabgt  2914  eqeu  2943  mob2  2953  mob  2955  euind  2960  reu6  2962  reuind  2978  sbctt  3065  rspsbca  3082  sbcnestgf  3145  rspcsbela  3153  ssel2  3188  sselda  3193  sstr  3201  nssne1  3251  nssne2  3252  reuss2  3453  reupick  3457  reupick2  3459  reximdva0m  3476  ssn0  3503  disjel  3515  ssdisj  3517  absneu  3705  preqr1g  3807  prel12  3812  dfiun2g  3959  nbrne1  4063  nbrne2  4064  mpteq12f  4124  triun  4155  csbexga  4172  iinexgm  4198  prexg  4255  copsex2t  4289  swopo  4353  poirr  4354  potr  4355  pofun  4359  issod  4366  ordelss  4426  trssord  4427  limelon  4446  trsuc  4469  eusvnfb  4501  rabxfrd  4516  regexmidlem1  4581  nordeq  4592  suc11g  4605  nnsuc  4664  brrelex12  4713  vtoclr  4723  optocl  4751  relop  4828  brcogw  4847  breldmg  4884  elreldm  4904  riinint  4939  issref  5065  xpidtr  5073  trin2  5074  cnveqb  5138  funopg  5305  funssres  5313  fununi  5342  funimass2  5352  imain  5356  fnun  5382  fco  5441  opelf  5447  f0rn0  5470  f1oun  5542  fun11iun  5543  fv3  5599  ndmfvg  5607  fvelima  5630  fvopab3ig  5653  fvmptssdm  5664  fvmptf  5672  fvimacnv  5695  fmptco  5746  funfvima2  5817  funfvima3  5818  f1veqaeq  5838  f1ocnvfvrneq  5851  fliftfun  5865  isotr  5885  isoini  5887  isopolem  5891  isosolem  5893  moriotass  5928  acexmidlem2  5941  suppssfv  6154  suppssov1  6155  f1dmex  6201  releldm2  6271  f1o2ndf1  6314  poxp  6318  tposf2  6354  iunon  6370  smoel2  6389  tfrlem9  6405  tfrexlem  6420  tfr1onlembxssdm  6429  tfr1onlemres  6435  tfrcllembxssdm  6442  tfrcllemres  6448  tfrcl  6450  tfri3  6453  frecabcl  6485  sucinc2  6532  nnacom  6570  nnmcom  6575  nnsucsssuc  6578  nnsucuniel  6581  nntri2or2  6584  nnaordi  6594  nnmordi  6602  nnaordex  6614  nnm00  6616  ectocld  6688  iinerm  6694  th3qlem2  6725  elpm2r  6753  mapsncnv  6782  mptelixpg  6821  ixpsnf1o  6823  f1oen4g  6843  f1dom4g  6844  f1oen3g  6845  f1oeng  6848  en2d  6859  en3d  6860  dom2lem  6863  fundmen  6898  fundmeng  6899  unen  6908  rex2dom  6910  xpdom2  6926  xpdom2g  6927  fopwdom  6933  nneneq  6954  phpm  6962  phpelm  6963  dif1enen  6977  fin0  6982  findcard  6985  diffifi  6991  ac6sfi  6995  onunsnss  7014  fiintim  7028  xpfi  7029  infidc  7036  fidcenum  7058  sbthlem1  7059  sbthlemi3  7061  sbthlemi10  7068  elfir  7075  isotilem  7108  inflbti  7126  ordiso2  7137  eldju2ndl  7174  eldju2ndr  7175  updjudhf  7181  mkvprop  7260  carden2bex  7297  pm54.43  7298  exmidfodomrlemeldju  7307  exmidfodomrlemreseldju  7308  exmidfodomrlemim  7309  ltmpig  7452  enq0sym  7545  addnq0mo  7560  mulnq0mo  7561  prarloclem3step  7609  prarloclem3  7610  genpml  7630  genpmu  7631  genprndl  7634  genprndu  7635  genpdisj  7636  distrlem1prl  7695  distrlem1pru  7696  distrlem4prl  7697  distrlem4pru  7698  distrlem5prl  7699  distrlem5pru  7700  ltsopr  7709  ltaddpr  7710  addcanprleml  7727  addcanprlemu  7728  recexprlemm  7737  recexprlemlol  7739  recexprlemupu  7741  aptiprleml  7752  aptiprlemu  7753  caucvgprlemnkj  7779  caucvgprlemnbj  7780  addsrmo  7856  mulsrmo  7857  srpospr  7896  caucvgsr  7915  axprecex  7993  mpomulf  8062  mulgt0  8147  ltne  8157  cnegexlem1  8247  cnegexlem2  8248  negf1o  8454  addgt0  8521  addgegt0  8522  addgtge0  8523  addge0  8524  recexre  8651  mulge0  8692  recexap  8726  prodgt02  8926  prodge02  8928  ltmul12a  8933  mulgt1  8936  nndivtr  9078  addltmul  9274  elnnnn0b  9339  xnn0nnn0pnf  9371  elnnz  9382  zmulcl  9426  nn0n0n1ge2  9443  nn0lt2  9454  nn0le2is012  9455  uzind2  9485  nn0ind-raph  9490  eluzp1m1  9672  uz3m2nn  9694  supinfneg  9716  infsupneg  9717  infregelbex  9719  negm  9736  lbzbi  9737  qaddcl  9756  qmulcl  9758  qreccl  9763  elpq  9770  ledivge1le  9848  nn0ledivnn  9889  xrltne  9935  xrre  9942  xrre2  9943  xrre3  9944  ge0gtmnf  9945  xltnegi  9957  xnn0xadd0  9989  xnegdi  9990  xposdif  10004  xlesubadd  10005  iccsupr  10088  icoshft  10112  icoshftf1o  10113  fznlem  10163  fzen  10165  uzsubsubfz  10169  fzsuc2  10201  elfz1b  10212  elfz0ubfz0  10247  elfz0fzfz0  10248  fz0fzelfz0  10249  fz0fzdiffz0  10252  elfzmlbp  10254  difelfznle  10257  fzofzim  10312  elincfzoext  10322  eluzgtdifelfzo  10326  elfzodifsumelfzo  10330  elfzonlteqm1  10339  elfzom1p1elfzo  10343  ssfzo12bi  10354  subfzo0  10371  zsupcllemex  10373  zssinfcl  10375  exbtwnzlemstep  10390  modqmuladdnn0  10513  modfzo0difsn  10540  addmodlteq  10543  frec2uzlt2d  10549  frecuzrdgtcl  10557  frecuzrdgfunlem  10564  seqf1og  10666  m1expcl2  10706  expge1  10721  leexp2r  10738  expubnd  10741  zesq  10803  expnlbnd  10809  nn0ltexp2  10854  nn0opthd  10867  faclbnd  10886  bcpasc  10911  hashprg  10953  seq3coll  10987  wrdnval  11024  wrdsymb0  11026  fstwrdne  11032  wrdred1hash  11037  swrdnd  11112  swrdwrdsymbg  11117  swrdsbslen  11119  swrdlsw  11122  rexanuz  11299  rexuz3  11301  r19.29uz  11303  r19.2uz  11304  absnid  11384  leabs  11385  ltabs  11398  icodiamlt  11491  maxleast  11524  negfi  11539  climcn2  11620  climcau  11658  climcaucn  11662  sumdc  11669  fsum3cvg  11689  isumz  11700  fsumf1o  11701  fisumss  11703  isumss2  11704  fsumzcl2  11716  fsumsplit  11718  fsumsplitsnun  11730  sumsplitdc  11743  fsum2dlemstep  11745  telfsumo  11777  fsumparts  11781  fsumiun  11788  isumrpcl  11805  fproddccvg  11883  prod1dc  11897  prodssdc  11900  fprodssdc  11901  prodsnf  11903  fprodsplitdc  11907  fprod2dlemstep  11933  fprodmodd  11952  efexp  11993  efieq1re  12083  p1modz1  12105  dvds0lem  12112  dvds2ln  12135  dvdssub2  12146  dvdsadd2b  12151  dvdsabseq  12158  divconjdvds  12160  dvdsdivcl  12161  odd2np1  12184  oddge22np1  12192  opoe  12206  omoe  12207  opeo  12208  omeo  12209  m1expo  12211  nn0ehalf  12214  nn0o1gt2  12216  nno  12217  divalgb  12236  ndvdsadd  12242  bitsinv1lem  12272  gcd0id  12300  gcdneg  12303  gcdaddm  12305  bezoutlemstep  12318  dfgcd2  12335  gcddiv  12340  dvdsmulgcd  12346  bezoutr  12353  bezoutr1  12354  uzwodc  12358  nninfctlemfo  12361  algfx  12374  lcmgcdlem  12399  lcmgcdeq  12405  coprmdvds  12414  divgcdcoprmex  12424  cncongr1  12425  cncongr2  12426  isprm3  12440  dvdsnprmd  12447  prmgt1  12454  oddprmgt2  12456  isprm6  12469  cncongrprm  12479  phibndlem  12538  phimullem  12547  powm2modprm  12575  modprm0  12577  modprmn0modprm0  12579  prm23lt5  12586  pcneg  12648  pcprmpw2  12656  dvdsprmpweqnn  12659  dvdsprmpweqle  12660  pcaddlem  12662  fldivp1  12671  pcfac  12673  oddprmdvds  12677  prmunb  12685  ennnfone  12796  unct  12813  lidrididd  13214  gsummgmpropd  13226  sgrpass  13240  issgrpd  13244  issubmnd  13274  imasmnd2  13284  mnd1id  13288  insubm  13317  dfgrp2  13359  grpid  13371  grpasscan1  13395  dfgrp3mlem  13430  dfgrp3me  13432  imasgrp2  13446  mulgnn0gsum  13464  mulgnn0p1  13469  mulgaddcom  13482  mulginvcom  13483  mulgass  13495  mulgpropdg  13500  subginv  13517  issubg2m  13525  issubg4m  13529  grpissubg  13530  resgrpisgrp  13531  subgintm  13534  kerf1ghm  13610  cmncom  13638  imasabl  13672  rngdi  13702  rngdir  13703  rngpropd  13717  imasrng  13718  imasring  13826  nzrunit  13950  issubrng2  13972  subrngintm  13974  issubrg2  14003  subrgintm  14005  lmodfopnelem1  14086  lmodfopnelem2  14087  lmodfopne  14088  islssm  14119  islidlm  14241  rnglidlmcl  14242  dflidl2rng  14243  rnglidlmmgm  14258  rnglidlmsgrp  14259  rnglidlrng  14260  dvdsrzring  14365  znidom  14419  uniopn  14473  istopon  14485  fiinbas  14521  tg2  14532  tgcl  14536  0nnei  14625  tgrest  14641  tgcn  14680  cnpnei  14691  cncnp2m  14703  lmtopcnp  14722  tx2cn  14742  txcn  14747  cnmpt21  14763  isxmet2d  14820  metrest  14978  metcnpi3  14989  tgioo  15026  fsumcncntop  15039  elcncf1di  15051  climcncf  15056  cncfco  15063  suplociccreex  15096  cnplimcim  15139  cnlimci  15145  reeff1olem  15243  efltlemlt  15246  zabsle1  15476  lgslem3  15479  lgsmod  15503  lgsdir2lem5  15509  lgsdir2  15510  lgsne0  15515  lgsdirnn0  15524  gausslemma2dlem0f  15531  gausslemma2dlem1a  15535  gausslemma2dlem3  15540  2lgslem1c  15567  2lgslem3a1  15574  2lgslem3b1  15575  2lgslem3c1  15576  2lgslem3d1  15577  2lgslem3  15578  2lgsoddprmlem2  15583  bj-charfun  15743  bj-charfunr  15746  bj-charfunbi  15747  bj-prexg  15847  peano5set  15876  bj-peano4  15891  bj-nn0suc  15900  bj-nn0sucALT  15914  bj-findis  15915  exmidsbthrlem  15961  trilpolemres  15981  trirec0  15983  nconstwlpolem  16004  neapmkv  16007