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  2787  rspcva  2839  rspc2va  2855  elabgt  2878  eqeu  2907  mob2  2917  mob  2919  euind  2924  reu6  2926  reuind  2942  sbctt  3029  rspsbca  3046  sbcnestgf  3108  rspcsbela  3116  ssel2  3150  sselda  3155  sstr  3163  nssne1  3213  nssne2  3214  reuss2  3415  reupick  3419  reupick2  3421  reximdva0m  3438  ssn0  3465  disjel  3477  ssdisj  3479  absneu  3664  preqr1g  3766  prel12  3771  dfiun2g  3918  nbrne1  4022  nbrne2  4023  mpteq12f  4083  triun  4114  csbexga  4131  iinexgm  4154  prexg  4211  copsex2t  4245  swopo  4306  poirr  4307  potr  4308  pofun  4312  issod  4319  ordelss  4379  trssord  4380  limelon  4399  trsuc  4422  eusvnfb  4454  rabxfrd  4469  regexmidlem1  4532  nordeq  4543  suc11g  4556  nnsuc  4615  brrelex12  4664  vtoclr  4674  optocl  4702  relop  4777  brcogw  4796  breldmg  4833  elreldm  4853  riinint  4888  issref  5011  xpidtr  5019  trin2  5020  cnveqb  5084  funopg  5250  funssres  5258  fununi  5284  funimass2  5294  imain  5298  fnun  5322  fco  5381  opelf  5387  f0rn0  5410  f1oun  5481  fun11iun  5482  fv3  5538  ndmfvg  5546  fvelima  5567  fvopab3ig  5590  fvmptssdm  5600  fvmptf  5608  fvimacnv  5631  fmptco  5682  funfvima2  5749  funfvima3  5750  f1veqaeq  5769  f1ocnvfvrneq  5782  fliftfun  5796  isotr  5816  isoini  5818  isopolem  5822  isosolem  5824  moriotass  5858  acexmidlem2  5871  suppssfv  6078  suppssov1  6079  f1dmex  6116  releldm2  6185  f1o2ndf1  6228  poxp  6232  tposf2  6268  iunon  6284  smoel2  6303  tfrlem9  6319  tfrexlem  6334  tfr1onlembxssdm  6343  tfr1onlemres  6349  tfrcllembxssdm  6356  tfrcllemres  6362  tfrcl  6364  tfri3  6367  frecabcl  6399  sucinc2  6446  nnacom  6484  nnmcom  6489  nnsucsssuc  6492  nnsucuniel  6495  nntri2or2  6498  nnaordi  6508  nnmordi  6516  nnaordex  6528  nnm00  6530  ectocld  6600  iinerm  6606  th3qlem2  6637  elpm2r  6665  mapsncnv  6694  mptelixpg  6733  ixpsnf1o  6735  f1oen3g  6753  f1oeng  6756  en2d  6767  en3d  6768  dom2lem  6771  fundmen  6805  fundmeng  6806  unen  6815  xpdom2  6830  xpdom2g  6831  fopwdom  6835  nneneq  6856  phpm  6864  phpelm  6865  dif1enen  6879  fin0  6884  findcard  6887  diffifi  6893  ac6sfi  6897  onunsnss  6915  fiintim  6927  xpfi  6928  fidcenum  6954  sbthlem1  6955  sbthlemi3  6957  sbthlemi10  6964  elfir  6971  isotilem  7004  inflbti  7022  ordiso2  7033  eldju2ndl  7070  eldju2ndr  7071  updjudhf  7077  mkvprop  7155  carden2bex  7187  pm54.43  7188  exmidfodomrlemeldju  7197  exmidfodomrlemreseldju  7198  exmidfodomrlemim  7199  ltmpig  7337  enq0sym  7430  addnq0mo  7445  mulnq0mo  7446  prarloclem3step  7494  prarloclem3  7495  genpml  7515  genpmu  7516  genprndl  7519  genprndu  7520  genpdisj  7521  distrlem1prl  7580  distrlem1pru  7581  distrlem4prl  7582  distrlem4pru  7583  distrlem5prl  7584  distrlem5pru  7585  ltsopr  7594  ltaddpr  7595  addcanprleml  7612  addcanprlemu  7613  recexprlemm  7622  recexprlemlol  7624  recexprlemupu  7626  aptiprleml  7637  aptiprlemu  7638  caucvgprlemnkj  7664  caucvgprlemnbj  7665  addsrmo  7741  mulsrmo  7742  srpospr  7781  caucvgsr  7800  axprecex  7878  mulgt0  8031  ltne  8041  cnegexlem1  8131  cnegexlem2  8132  negf1o  8338  addgt0  8404  addgegt0  8405  addgtge0  8406  addge0  8407  recexre  8534  mulge0  8575  recexap  8609  prodgt02  8809  prodge02  8811  ltmul12a  8816  mulgt1  8819  nndivtr  8960  addltmul  9154  elnnnn0b  9219  xnn0nnn0pnf  9251  elnnz  9262  zmulcl  9305  nn0n0n1ge2  9322  nn0lt2  9333  nn0le2is012  9334  uzind2  9364  nn0ind-raph  9369  eluzp1m1  9550  uz3m2nn  9572  supinfneg  9594  infsupneg  9595  infregelbex  9597  negm  9614  lbzbi  9615  qaddcl  9634  qmulcl  9636  qreccl  9641  elpq  9647  ledivge1le  9725  nn0ledivnn  9766  xrltne  9812  xrre  9819  xrre2  9820  xrre3  9821  ge0gtmnf  9822  xltnegi  9834  xnn0xadd0  9866  xnegdi  9867  xposdif  9881  xlesubadd  9882  iccsupr  9965  icoshft  9989  icoshftf1o  9990  fznlem  10040  fzen  10042  uzsubsubfz  10046  fzsuc2  10078  elfz1b  10089  elfz0ubfz0  10124  elfz0fzfz0  10125  fz0fzelfz0  10126  fz0fzdiffz0  10129  elfzmlbp  10131  difelfznle  10134  fzofzim  10187  eluzgtdifelfzo  10196  elfzodifsumelfzo  10200  elfzonlteqm1  10209  elfzom1p1elfzo  10213  ssfzo12bi  10224  subfzo0  10241  exbtwnzlemstep  10247  modqmuladdnn0  10367  modfzo0difsn  10394  addmodlteq  10397  frec2uzlt2d  10403  frecuzrdgtcl  10411  frecuzrdgfunlem  10418  m1expcl2  10541  expge1  10556  leexp2r  10573  expubnd  10576  zesq  10638  expnlbnd  10644  nn0ltexp2  10688  nn0opthd  10701  faclbnd  10720  bcpasc  10745  hashprg  10787  seq3coll  10821  rexanuz  10996  rexuz3  10998  r19.29uz  11000  r19.2uz  11001  absnid  11081  leabs  11082  ltabs  11095  icodiamlt  11188  maxleast  11221  negfi  11235  climcn2  11316  climcau  11354  climcaucn  11358  sumdc  11365  fsum3cvg  11385  isumz  11396  fsumf1o  11397  fisumss  11399  isumss2  11400  fsumzcl2  11412  fsumsplit  11414  fsumsplitsnun  11426  sumsplitdc  11439  fsum2dlemstep  11441  telfsumo  11473  fsumparts  11477  fsumiun  11484  isumrpcl  11501  fproddccvg  11579  prod1dc  11593  prodssdc  11596  fprodssdc  11597  prodsnf  11599  fprodsplitdc  11603  fprod2dlemstep  11629  fprodmodd  11648  efexp  11689  efieq1re  11778  p1modz1  11800  dvds0lem  11807  dvds2ln  11830  dvdssub2  11841  dvdsadd2b  11846  dvdsabseq  11852  divconjdvds  11854  dvdsdivcl  11855  odd2np1  11877  oddge22np1  11885  opoe  11899  omoe  11900  opeo  11901  omeo  11902  m1expo  11904  nn0ehalf  11907  nn0o1gt2  11909  nno  11910  divalgb  11929  ndvdsadd  11935  zsupcllemex  11946  zssinfcl  11948  gcd0id  11979  gcdneg  11982  gcdaddm  11984  bezoutlemstep  11997  dfgcd2  12014  gcddiv  12019  dvdsmulgcd  12025  bezoutr  12032  bezoutr1  12033  uzwodc  12037  algfx  12051  lcmgcdlem  12076  lcmgcdeq  12082  coprmdvds  12091  divgcdcoprmex  12101  cncongr1  12102  cncongr2  12103  isprm3  12117  dvdsnprmd  12124  prmgt1  12131  oddprmgt2  12133  isprm6  12146  cncongrprm  12156  phibndlem  12215  phimullem  12224  powm2modprm  12251  modprm0  12253  modprmn0modprm0  12255  prm23lt5  12262  pcneg  12323  pcprmpw2  12331  dvdsprmpweqnn  12334  dvdsprmpweqle  12335  pcaddlem  12337  fldivp1  12345  pcfac  12347  oddprmdvds  12351  prmunb  12359  ennnfone  12425  unct  12442  lidrididd  12800  sgrpass  12813  issubmnd  12842  mnd1id  12847  insubm  12871  dfgrp2  12901  grpid  12911  grpasscan1  12932  dfgrp3mlem  12967  dfgrp3me  12969  mulgnn0p1  12993  mulgaddcom  13005  mulginvcom  13006  mulgass  13018  mulgpropdg  13023  subginv  13039  issubg2m  13047  issubg4m  13051  grpissubg  13052  resgrpisgrp  13053  subgintm  13056  cmncom  13103  nzrunit  13327  issubrg2  13360  subrgintm  13362  dvdsrzring  13463  uniopn  13471  istopon  13483  fiinbas  13519  tg2  13530  tgcl  13534  0nnei  13623  tgrest  13639  tgcn  13678  cnpnei  13689  cncnp2m  13701  lmtopcnp  13720  tx2cn  13740  txcn  13745  cnmpt21  13761  isxmet2d  13818  metrest  13976  metcnpi3  13987  tgioo  14016  fsumcncntop  14026  elcncf1di  14036  climcncf  14041  cncfco  14048  suplociccreex  14072  cnplimcim  14106  cnlimci  14112  reeff1olem  14162  efltlemlt  14165  zabsle1  14370  lgslem3  14373  lgsmod  14397  lgsdir2lem5  14403  lgsdir2  14404  lgsne0  14409  lgsdirnn0  14418  2lgsoddprmlem2  14424  bj-charfun  14529  bj-charfunr  14532  bj-charfunbi  14533  bj-prexg  14633  peano5set  14662  bj-peano4  14677  bj-nn0suc  14686  bj-nn0sucALT  14700  bj-findis  14701  exmidsbthrlem  14740  trilpolemres  14760  trirec0  14762  nconstwlpolem  14782  neapmkv  14785