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  413  sylan9r  414  imdistani  449  mpan10  478  adantl4r  521  adantl5r  529  adantl6r  530  a2and  564  anabsi5  585  anim12dan  608  pm3.43  610  con3dimp  644  annimim  697  imnan  701  jaoian  807  jaodan  809  stdcndc  857  impidc  870  pm2.5gdc  878  con2bidc  887  pm5.18dc  895  dfandc  896  pm4.63dc  898  pm4.54dc  914  pm4.79dc  915  orcanai  940  annimdc  950  pm4.55dc  951  orandc  952  pm4.82  963  pm3.11dc  970  pm3.12dc  971  dn1dc  973  3jcad  1209  3expia  1236  3an1rs  1250  3imp1  1251  3imp2  1253  syl3anl2  1327  3jaoian  1346  3jaodan  1347  mp3anl1  1372  mp3anl2  1373  mp3anl3  1374  ecased  1390  xor3dc  1436  pm5.15dc  1438  xor2dc  1439  xornbidc  1440  xordc  1441  nbbndc  1443  biassdc  1444  bilukdc  1445  dfbi3dc  1446  pm5.24dc  1447  xordidc  1448  alanimi  1512  19.29  1673  equs4  1777  equsexd  1782  spimth  1788  equs5a  1847  ax11v2  1873  ax11b  1879  equs5or  1883  sb5rf  1905  equvin  1916  nfsb4t  2074  eu5  2134  mopick  2165  euexex  2172  2euswapdc  2178  exists2  2184  eqrdav  2237  dvelimdc  2413  nebidc  2500  pm13.18  2501  nelne1  2510  nelne2  2511  rspa  2598  ralrimdvv  2634  r19.21bi  2638  r19.26  2677  ralbi  2683  rexbi  2684  r19.29  2688  vtoclgft  2873  rspcva  2927  rspc2va  2944  elabgt  2967  eqeu  2996  mob2  3006  mob  3008  euind  3013  reu6  3015  reuind  3031  sbctt  3118  rspsbca  3136  sbcnestgf  3199  rspcsbela  3207  ssel2  3243  sselda  3248  sstr  3256  nssne1  3306  nssne2  3307  reuss2  3513  reupick  3517  reupick2  3519  reximdva0m  3537  ssn0  3565  disjel  3578  ssdisj  3580  ifeqeqxdc  3684  absneu  3779  preqr1g  3886  prel12  3891  dfiun2g  4039  nbrne1  4144  nbrne2  4145  mpteq12f  4206  triun  4237  csbexga  4256  prcssprc  4269  iinexgm  4285  prexg  4344  copsex2t  4380  swopo  4446  poirr  4447  potr  4448  pofun  4452  issod  4459  ordelss  4519  trssord  4520  limelon  4539  trsuc  4562  eusvnfb  4595  rabxfrd  4610  regexmidlem1  4675  nordeq  4686  suc11g  4699  nnsuc  4758  brrelex12  4808  vtoclr  4818  optocl  4846  relop  4925  brcogw  4944  breldmg  4982  elreldm  5003  riinint  5038  xpexcnvm  5137  issref  5165  xpidtr  5173  trin2  5174  cnveqb  5238  funopg  5406  funssres  5415  fununi  5444  funimass2  5454  imain  5458  fnun  5484  fco  5547  opelf  5555  f0rn0  5582  f1oun  5654  fun11iun  5655  fv3  5713  ndmfvg  5721  fvelima  5748  fvopab3ig  5773  fvmptssdm  5784  fvmptf  5792  fvimacnv  5815  fmptco  5865  fcof  5885  funfvima2  5941  funfvima3  5942  f1veqaeq  5965  f1ocnvfvrneq  5978  fliftfun  5992  isotr  6012  isoini  6014  isopolem  6018  isosolem  6020  moriotass  6059  acexmidlem2  6072  suppssov1  6289  f1dmex  6335  elabreximd  6346  releldm2  6409  f1o2ndf1  6454  poxp  6458  fsuppeq  6477  suppssfvg  6493  tposf2  6529  iunon  6545  smoel2  6564  tfrlem9  6580  tfrexlem  6595  tfr1onlembxssdm  6604  tfr1onlemres  6610  tfrcllembxssdm  6617  tfrcllemres  6623  tfrcl  6625  tfri3  6628  frecabcl  6660  sucinc2  6709  nnacom  6747  nnmcom  6752  nnsucsssuc  6755  nnsucuniel  6758  nntri2or2  6761  nnaordi  6771  nnmordi  6779  nnaordex  6791  nnm00  6793  ectocld  6865  iinerm  6871  th3qlem2  6902  elpm2r  6930  mapsnd  6960  mapsncnv  6967  mptelixpg  7006  ixpsnf1o  7008  f1oen4g  7028  f1dom4g  7029  f1oen3g  7030  f1oeng  7033  en2d  7044  en3d  7045  dom2lem  7048  fundmen  7084  fundmeng  7085  unen  7095  modom  7098  rex2dom  7100  en2m  7103  xpdom2  7119  xpdom2g  7120  fopwdom  7126  nneneq  7148  phpm  7157  phpelm  7158  dif1enen  7174  fin0  7179  findcard  7182  diffifi  7188  ac6sfi  7192  onunsnss  7214  fiintim  7228  xpfi  7229  infidc  7238  fidcenum  7263  sbthlem1  7264  sbthlemi3  7266  sbthlemi10  7273  ffsuppbi  7290  elfir  7297  isotilem  7336  inflbti  7354  ordiso2  7365  eldju2ndl  7402  eldju2ndr  7403  updjudhf  7409  mkvprop  7488  carden2bex  7525  pm54.43  7526  exmidfodomrlemeldju  7541  exmidfodomrlemreseldju  7542  exmidfodomrlemim  7543  pw1m  7573  ltmpig  7696  enq0sym  7789  addnq0mo  7804  mulnq0mo  7805  prarloclem3step  7853  prarloclem3  7854  genpml  7874  genpmu  7875  genprndl  7878  genprndu  7879  genpdisj  7880  distrlem1prl  7939  distrlem1pru  7940  distrlem4prl  7941  distrlem4pru  7942  distrlem5prl  7943  distrlem5pru  7944  ltsopr  7953  ltaddpr  7954  addcanprleml  7971  addcanprlemu  7972  recexprlemm  7981  recexprlemlol  7983  recexprlemupu  7985  aptiprleml  7996  aptiprlemu  7997  caucvgprlemnkj  8023  caucvgprlemnbj  8024  addsrmo  8100  mulsrmo  8101  srpospr  8140  caucvgsr  8159  axprecex  8237  mpomulf  8306  mulgt0  8390  ltne  8400  cnegexlem1  8491  cnegexlem2  8492  negf1o  8699  addgt0  8766  addgegt0  8767  addgtge0  8768  addge0  8769  recexre  8896  mulge0  8937  recexap  8971  prodgt02  9173  prodge02  9175  ltmul12a  9180  mulgt1  9183  nndivtr  9325  addltmul  9521  elnnnn0b  9586  fcdmnn0supp  9594  fcdmnn0fsupp  9595  fcdmnn0suppg  9596  xnn0nnn0pnf  9622  elnnz  9633  zmulcl  9677  nn0n0n1ge2  9694  nn0lt2  9706  nn0le2is012  9707  uzind2  9737  nn0ind-raph  9742  eluzp1m1  9925  uz3m2nn  9952  supinfneg  9974  infsupneg  9975  infregelbex  9977  negm  9994  lbzbi  9995  qaddcl  10014  qmulcl  10016  qreccl  10021  elpq  10028  ledivge1le  10106  nn0ledivnn  10147  xrltne  10194  xrre  10201  xrre2  10202  xrre3  10203  ge0gtmnf  10204  xltnegi  10216  xnn0xadd0  10248  xnegdi  10249  xposdif  10263  xlesubadd  10264  iccsupr  10347  icoshft  10371  icoshftf1o  10372  fznlem  10424  fzen  10426  uzsubsubfz  10430  fzsuc2  10464  elfz1b  10475  elfz0ubfz0  10510  elfz0fzfz0  10511  fz0fzelfz0  10512  fz0fzdiffz0  10515  elfzmlbp  10517  difelfznle  10520  nn0p1elfzo  10572  fzofzim  10578  elincfzoext  10589  eluzgtdifelfzo  10593  elfzodifsumelfzo  10597  elfzonlteqm1  10606  elfzom1p1elfzo  10610  ssfzo12bi  10621  subfzo0  10639  zsupcllemex  10641  zssinfcl  10643  exbtwnzlemstep  10660  modqmuladdnn0  10783  modfzo0difsn  10810  addmodlteq  10813  frec2uzlt2d  10819  frecuzrdgtcl  10827  frecuzrdgfunlem  10834  seqf1og  10936  m1expcl2  10976  expge1  10991  leexp2r  11008  expubnd  11011  zesq  11074  expnlbnd  11080  nn0ltexp2  11125  nn0opthd  11138  faclbnd  11157  bcpasc  11182  hashprg  11227  hashf1  11265  seq3coll  11272  wrdnval  11313  wrdsymb0  11315  fstwrdne  11321  wrdred1hash  11326  swrdnd  11409  swrdwrdsymbg  11414  swrdsbslen  11416  swrdlsw  11419  swrdswrdlem  11454  swrdswrd  11455  pfxswrd  11456  cats1un  11471  wrd2ind  11473  swrdccatin1  11475  pfxccatin12lem4  11476  pfxccatin12lem2a  11477  pfxccatin12lem1  11478  swrdccatin2  11479  pfxccatin12lem2c  11480  pfxccatin12lem2  11481  pfxccatin12lem3  11482  pfxccatin12  11483  pfxccat3  11484  swrdccat  11485  pfxccat3a  11488  swrdccat3blem  11489  swrdccat3b  11490  swrdccatin2d  11494  reuccatpfxs1lem  11496  rexanuz  11732  rexuz3  11734  r19.29uz  11736  r19.2uz  11737  absnid  11817  leabs  11818  ltabs  11831  icodiamlt  11924  maxleast  11957  negfi  11972  climcn2  12053  climcau  12091  climcaucn  12095  sumdc  12102  fsum3cvg  12123  isumz  12134  fsumf1o  12135  fisumss  12137  isumss2  12138  fsumzcl2  12150  fsumsplit  12152  fsumsplitsnun  12164  sumsplitdc  12177  fsum2dlemstep  12179  telfsumo  12211  fsumparts  12215  fsumiun  12222  isumrpcl  12239  fproddccvg  12317  prod1dc  12331  prodssdc  12334  fprodssdc  12335  prodsnf  12337  fprodsplitdc  12341  fprod2dlemstep  12367  fprodmodd  12386  efexp  12427  efieq1re  12517  p1modz1  12539  dvds0lem  12546  dvds2ln  12569  dvdssub2  12580  dvdsadd2b  12585  dvdsabseq  12592  divconjdvds  12594  dvdsdivcl  12595  odd2np1  12618  oddge22np1  12626  opoe  12640  omoe  12641  opeo  12642  omeo  12643  m1expo  12645  nn0ehalf  12648  nn0o1gt2  12650  nno  12651  divalgb  12670  ndvdsadd  12676  bitsinv1lem  12706  gcd0id  12734  gcdneg  12737  gcdaddm  12739  bezoutlemstep  12752  dfgcd2  12769  gcddiv  12774  dvdsmulgcd  12780  bezoutr  12787  bezoutr1  12788  uzwodc  12792  nninfctlemfo  12795  algfx  12808  lcmgcdlem  12833  lcmgcdeq  12839  coprmdvds  12848  divgcdcoprmex  12858  cncongr1  12859  cncongr2  12860  isprm3  12874  dvdsnprmd  12881  prmgt1  12888  oddprmgt2  12890  isprm6  12903  cncongrprm  12913  phibndlem  12972  phimullem  12981  powm2modprm  13009  modprm0  13011  modprmn0modprm0  13013  prm23lt5  13020  pcneg  13082  pcprmpw2  13090  dvdsprmpweqnn  13093  dvdsprmpweqle  13094  pcaddlem  13096  fldivp1  13105  pcfac  13107  oddprmdvds  13111  prmunb  13119  ballotfilemfc0  13210  ballotfilemfcc  13211  ballotfilem4  13219  ballotfilemi1  13223  ballotfilemii  13224  ballotfilemic  13228  ballotfilem1c  13229  ballotfilemirc  13253  ballotfilem7  13257  ennnfone  13294  unct  13311  lidrididd  13679  sgrpass  13700  issgrpd  13704  issubmnd  13732  imasmnd2  13736  mnd1id  13740  insubm  13769  dfgrp2  13809  grpid  13821  grpasscan1  13845  dfgrp3mlem  13880  dfgrp3me  13882  imasgrp2  13890  mulgnn0gzsum  13908  mulgnn0p1  13913  mulgaddcom  13926  mulginvcom  13927  mulgass  13939  mulgpropdg  13944  subginv  13961  issubg2m  13969  issubg4m  13973  grpissubg  13974  resgrpisgrp  13975  subgintm  13978  kerf1ghm  14054  cmncom  14082  imasabl  14117  gsumvalfi  14129  rngdi  14214  rngdir  14215  rngpropd  14229  imasrng  14230  rng1zrlem  14233  imasring  14342  nzrunit  14468  issubrng2  14491  subrngintm  14493  issubrg2  14522  subrgintm  14524  lmodfopnelem1  14633  lmodfopnelem2  14634  lmodfopne  14635  islssm  14666  islidlm  14788  rnglidlmcl  14789  dflidl2rng  14790  rnglidlmmgm  14805  rnglidlmsgrp  14806  rnglidlrng  14807  gsumfsum  14895  dvdsrzring  14910  znidom  14964  uniopn  15025  istopon  15037  fiinbas  15073  tg2  15084  tgcl  15088  0nnei  15177  tgrest  15193  tgcn  15232  cnpnei  15243  cncnp2m  15255  lmtopcnp  15274  tx2cn  15294  txcn  15299  cnmpt21  15315  isxmet2d  15372  metrest  15530  metcnpi3  15541  tgioo  15578  fsumcncntop  15591  elcncf1di  15603  climcncf  15608  cncfco  15615  suplociccreex  15648  cnplimcim  15691  cnlimci  15697  reeff1olem  15795  efltlemlt  15798  pellexlem1  16005  zabsle1  16032  lgslem3  16035  lgsmod  16059  lgsdir2lem5  16065  lgsdir2  16066  lgsne0  16071  lgsdirnn0  16080  gausslemma2dlem0f  16087  gausslemma2dlem1a  16091  gausslemma2dlem3  16096  2lgslem1c  16123  2lgslem3a1  16130  2lgslem3b1  16131  2lgslem3c1  16132  2lgslem3d1  16133  2lgslem3  16134  2lgsoddprmlem2  16139  uhgrm  16233  incistruhgr  16245  upgrfnen  16253  umgrfnen  16263  umgrnloop  16271  upgredgpr  16304  usgrausgrben  16327  usgredgop  16328  usgruspgrben  16341  usgrislfuspgrdom  16345  umgrvad2edg  16366  ushgredgedg  16381  ushgredgedgloop  16383  uhgr0v0e  16389  subgreldmiedg  16424  subupgr  16428  uhgrspansubgrlem  16431  vtxdg0v  16449  wlkpropg  16479  wlkvg  16483  wlkl1loop  16513  upgriswlkdc  16515  upgrwlkedg  16516  upgrwlkvtxedg  16519  uspgr2wlkeq  16520  wlkres  16534  trlf1  16543  clwwlk1loop  16554  clwwlkccatlem  16555  isclwwlknx  16571  clwwlkn1loopb  16575  clwwlkext2edg  16577  umgr2cwwk2dif  16579  clwwlknonex2lem2  16593  clwwlknonex2  16594  eupthseg  16607  eupth2lem3lem4fi  16628  bj-charfun  16747  bj-charfunr  16750  bj-charfunbi  16751  bj-prexg  16851  peano5set  16880  bj-peano4  16895  bj-nn0suc  16904  bj-nn0sucALT  16918  bj-findis  16919  exmidsbthrlem  16972  trilpolemres  16996  trirec0  16998  nconstwlpolem  17020  neapmkv  17023