Theorem imp 122

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 107	. 2 |- ( ( ph /\ ps ) -> ph )
2		simpr 108	. 2 |- ( ( ph /\ ps ) -> ps )
3		imp.1	. 2 |- ( ph -> ( ps -> ch ) )
4	1, 2, 3	sylc 61	1 |- ( ( ph /\ ps ) -> ch )

Syntax hints:   -> wi 4   /\ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105

This theorem is referenced by:  impcom  123  impd  251  imp31  252  imp32  253  expdimp  255  impancom  256  pm3.22  261  ancoms  264  adantr  270  impel  274  biimpa  290  biimpar  291  biimpac  292  biimparc  293  pm3.33  337  pm3.34  338  pm3.35  339  pm5.31  340  imp4b  342  imp41  345  imp42  346  imp43  347  imp44  348  imp45  349  imp5g  352  expr  367  impac  373  sylan9  401  sylan9r  402  imdistani  433  mpan10  457  anabsi5  543  anim12dan  564  pm3.43  566  con3dimp  596  imnan  656  jaoian  741  jaodan  743  impidc  788  pm2.5dc  796  con2bidc  802  pm5.18dc  810  dfandc  811  pm4.63dc  813  annimim  815  pm4.54dc  838  pm4.79dc  842  orcanai  870  annimdc  878  pm4.55dc  879  orandc  880  pm4.82  891  pm3.11dc  898  pm3.12dc  899  dn1dc  901  3jcad  1119  3expia  1140  3an1rs  1150  3imp1  1151  3imp2  1153  syl3anl2  1218  3jaoian  1236  3jaodan  1237  mp3anl1  1262  mp3anl2  1263  mp3anl3  1264  ecased  1280  xor3dc  1318  pm5.15dc  1320  xor2dc  1321  xornbidc  1322  xordc  1323  nbbndc  1325  biassdc  1326  bilukdc  1327  dfbi3dc  1328  pm5.24dc  1329  xordidc  1330  alanimi  1388  19.29  1551  equs4  1653  equsexd  1657  spimth  1663  equs5a  1715  ax11v2  1741  ax11b  1747  equs5or  1751  sb5rf  1773  equvin  1784  nfsb4t  1931  eu5  1988  mopick  2019  euexex  2026  2euswapdc  2032  exists2  2038  eqrdav  2080  dvelimdc  2238  nebidc  2325  pm13.18  2326  nelne1  2335  nelne2  2336  ralrimdvv  2445  r19.21bi  2449  r19.26  2485  ralbi  2489  rexbi  2490  r19.29  2494  vtoclgft  2649  rspcva  2699  rspc2va  2714  elabgt  2735  eqeu  2762  mob2  2772  mob  2774  euind  2779  reu6  2781  reuind  2795  sbctt  2880  rspsbca  2897  sbcnestgf  2953  rspcsbela  2961  ssel2  2994  sselda  2999  sstr  3007  nssne1  3055  nssne2  3056  reuss2  3244  reupick  3248  reupick2  3250  reximdva0m  3263  ssn0  3286  disjel  3298  ssdisj  3300  absneu  3464  preqr1g  3558  prel12  3563  dfiun2g  3710  nbrne1  3802  nbrne2  3803  mpteq12f  3858  triun  3888  csbexga  3906  iinexgm  3929  prexg  3966  copsex2t  4000  swopo  4061  poirr  4062  potr  4063  pofun  4067  issod  4074  ordelss  4134  trssord  4135  limelon  4154  trsuc  4177  eusvnfb  4204  rabxfrd  4219  regexmidlem1  4276  nordeq  4287  suc11g  4300  nnsuc  4356  brrelex12  4399  vtoclr  4406  optocl  4434  relop  4504  brcogw  4522  breldmg  4559  elreldm  4578  riinint  4611  issref  4727  xpidtr  4735  trin2  4736  cnveqb  4796  funopg  4954  funssres  4962  fununi  4987  funimass2  4997  imain  5001  fnun  5025  fco  5076  opelf  5082  f1oun  5166  fun11iun  5167  fv3  5218  ndmfvg  5225  fvelima  5246  fvopab3ig  5267  fvmptssdm  5276  fvmptf  5284  fvimacnv  5303  fmptco  5351  funfvima2  5412  funfvima3  5413  f1veqaeq  5429  f1ocnvfvrneq  5442  fliftfun  5456  isotr  5476  isoini  5477  isopolem  5481  isosolem  5483  moriotass  5516  acexmidlem2  5529  suppssfv  5728  suppssov1  5729  f1dmex  5763  releldm2  5831  f1o2ndf1  5869  poxp  5873  tposf2  5906  iunon  5922  smoel2  5941  tfrlem9  5958  tfrexlem  5971  tfri3  5976  sucinc2  6049  nnacom  6086  nnmcom  6091  nnsucsssuc  6094  nntri2or2  6099  nnaordi  6104  nnmordi  6112  nnaordex  6123  nnm00  6125  ectocld  6195  iinerm  6201  th3qlem2  6232  f1oen3g  6257  f1oeng  6260  en2d  6271  en3d  6272  dom2lem  6275  fundmen  6309  fundmeng  6310  unen  6316  xpdom2  6328  xpdom2g  6329  fopwdom  6333  nneneq  6343  phpm  6351  phpelm  6352  fin0  6369  findcard  6372  diffifi  6378  ac6sfi  6379  onunsnss  6383  isotilem  6419  inflbti  6437  ordiso2  6446  carden2bex  6458  pm54.43  6459  ltmpig  6529  enq0sym  6622  addnq0mo  6637  mulnq0mo  6638  prarloclem3step  6686  prarloclem3  6687  genpml  6707  genpmu  6708  genprndl  6711  genprndu  6712  genpdisj  6713  distrlem1prl  6772  distrlem1pru  6773  distrlem4prl  6774  distrlem4pru  6775  distrlem5prl  6776  distrlem5pru  6777  ltsopr  6786  ltaddpr  6787  addcanprleml  6804  addcanprlemu  6805  recexprlemm  6814  recexprlemlol  6816  recexprlemupu  6818  aptiprleml  6829  aptiprlemu  6830  caucvgprlemnkj  6856  caucvgprlemnbj  6857  addsrmo  6920  mulsrmo  6921  srpospr  6959  caucvgsr  6978  axprecex  7046  mulgt0  7186  ltne  7196  cnegexlem1  7283  cnegexlem2  7284  negf1o  7486  addgt0  7552  addgegt0  7553  addgtge0  7554  addge0  7555  recexre  7678  mulge0  7719  recexap  7743  prodgt02  7931  prodge02  7933  ltmul12a  7938  mulgt1  7941  nndivtr  8080  addltmul  8267  elnnnn0b  8332  elnnz  8361  zmulcl  8404  nn0n0n1ge2  8418  nn0lt2  8429  uzind2  8459  nn0ind-raph  8464  eluzp1m1  8642  uz3m2nn  8661  supinfneg  8683  infsupneg  8684  negm  8700  lbzbi  8701  qaddcl  8720  qmulcl  8722  qreccl  8727  ledivge1le  8803  nn0ledivnn  8838  xrltne  8883  xrre  8887  xrre2  8888  xrre3  8889  ge0gtmnf  8890  xltnegi  8902  iccsupr  8989  icoshft  9012  icoshftf1o  9013  fznlem  9060  fzen  9062  uzsubsubfz  9066  fzsuc2  9096  elfz1b  9107  elfz0ubfz0  9136  elfz0fzfz0  9137  fz0fzelfz0  9138  fz0fzdiffz0  9141  elfzmlbp  9143  difelfznle  9146  fzofzim  9197  eluzgtdifelfzo  9206  elfzodifsumelfzo  9210  elfzonlteqm1  9219  elfzom1p1elfzo  9223  ssfzo12bi  9234  subfzo0  9251  modqmuladdnn0  9370  modfzo0difsn  9397  addmodlteq  9400  frec2uzlt2d  9406  frecuzrdgfn  9414  iseqid3  9465  m1expcl2  9498  expge1  9513  leexp2r  9530  expubnd  9533  zesq  9591  expnlbnd  9597  nn0opthd  9649  faclbnd  9668  bcpasc  9693  rexanuz  9874  rexuz3  9876  r19.29uz  9878  r19.2uz  9879  absnid  9959  leabs  9960  ltabs  9973  icodiamlt  10066  maxleast  10099  negfi  10110  climcn2  10148  climcau  10184  climcaucn  10188  dvds0lem  10205  dvds2ln  10228  dvdssub2  10237  dvdsadd2b  10242  dvdsabseq  10247  divconjdvds  10249  dvdsdivcl  10250  odd2np1  10272  oddge22np1  10281  opoe  10295  omoe  10296  opeo  10297  omeo  10298  m1expo  10300  nn0ehalf  10303  nn0o1gt2  10305  nno  10306  divalgb  10325  ndvdsadd  10331  zsupcllemex  10342  zssinfcl  10344  gcd0id  10370  gcdneg  10373  gcdaddm  10375  bezoutlemstep  10386  dfgcd2  10403  gcddiv  10408  dvdsmulgcd  10414  bezoutr  10421  bezoutr1  10422  ialgfx  10434  lcmgcdlem  10459  lcmgcdeq  10465  coprmdvds  10474  divgcdcoprmex  10484  cncongr1  10485  cncongr2  10486  isprm3  10500  dvdsnprmd  10507  prmgt1  10513  oddprmgt2  10515  isprm6  10526  cncongrprm  10536  bj-prexg  10702  peano5set  10735  bj-peano4  10750  bj-nn0suc  10759  bj-nn0sucALT  10773  bj-findis  10774