Theorem imp 123

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 108	. 2 |- ( ( ph /\ ps ) -> ph )
2		simpr 109	. 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 103

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

This theorem is referenced by:  impcom  124  impd  252  imp31  254  imp32  255  expdimp  257  impancom  258  pm3.22  263  ancoms  266  adantr  274  impel  278  biimpa  294  biimpar  295  biimpac  296  biimparc  297  pm3.33  343  pm3.34  344  pm3.35  345  pm5.31  346  imp4b  348  imp41  351  imp42  352  imp43  353  imp44  354  imp45  355  imp5g  358  expr  373  impac  379  sylan9  407  sylan9r  408  imdistani  443  mpan10  471  adantl4r  514  adantl5r  522  adantl6r  523  a2and  553  anabsi5  574  anim12dan  595  pm3.43  597  con3dimp  630  annimim  681  imnan  685  jaoian  790  jaodan  792  stdcndc  840  impidc  853  pm2.5gdc  861  con2bidc  870  pm5.18dc  878  dfandc  879  pm4.63dc  881  pm4.54dc  897  pm4.79dc  898  orcanai  923  annimdc  932  pm4.55dc  933  orandc  934  pm4.82  945  pm3.11dc  952  pm3.12dc  953  dn1dc  955  3jcad  1173  3expia  1200  3an1rs  1214  3imp1  1215  3imp2  1217  syl3anl2  1282  3jaoian  1300  3jaodan  1301  mp3anl1  1326  mp3anl2  1327  mp3anl3  1328  ecased  1344  xor3dc  1382  pm5.15dc  1384  xor2dc  1385  xornbidc  1386  xordc  1387  nbbndc  1389  biassdc  1390  bilukdc  1391  dfbi3dc  1392  pm5.24dc  1393  xordidc  1394  alanimi  1452  19.29  1613  equs4  1718  equsexd  1722  spimth  1728  equs5a  1787  ax11v2  1813  ax11b  1819  equs5or  1823  sb5rf  1845  equvin  1856  nfsb4t  2007  eu5  2066  mopick  2097  euexex  2104  2euswapdc  2110  exists2  2116  eqrdav  2169  dvelimdc  2333  nebidc  2420  pm13.18  2421  nelne1  2430  nelne2  2431  rspa  2518  ralrimdvv  2554  r19.21bi  2558  r19.26  2596  ralbi  2602  rexbi  2603  r19.29  2607  vtoclgft  2780  rspcva  2832  rspc2va  2848  elabgt  2871  eqeu  2900  mob2  2910  mob  2912  euind  2917  reu6  2919  reuind  2935  sbctt  3021  rspsbca  3038  sbcnestgf  3100  rspcsbela  3108  ssel2  3142  sselda  3147  sstr  3155  nssne1  3205  nssne2  3206  reuss2  3407  reupick  3411  reupick2  3413  reximdva0m  3430  ssn0  3457  disjel  3469  ssdisj  3471  absneu  3655  preqr1g  3753  prel12  3758  dfiun2g  3905  nbrne1  4008  nbrne2  4009  mpteq12f  4069  triun  4100  csbexga  4117  iinexgm  4140  prexg  4196  copsex2t  4230  swopo  4291  poirr  4292  potr  4293  pofun  4297  issod  4304  ordelss  4364  trssord  4365  limelon  4384  trsuc  4407  eusvnfb  4439  rabxfrd  4454  regexmidlem1  4517  nordeq  4528  suc11g  4541  nnsuc  4600  brrelex12  4649  vtoclr  4659  optocl  4687  relop  4761  brcogw  4780  breldmg  4817  elreldm  4837  riinint  4872  issref  4993  xpidtr  5001  trin2  5002  cnveqb  5066  funopg  5232  funssres  5240  fununi  5266  funimass2  5276  imain  5280  fnun  5304  fco  5363  opelf  5369  f0rn0  5392  f1oun  5462  fun11iun  5463  fv3  5519  ndmfvg  5527  fvelima  5548  fvopab3ig  5570  fvmptssdm  5580  fvmptf  5588  fvimacnv  5611  fmptco  5662  funfvima2  5728  funfvima3  5729  f1veqaeq  5748  f1ocnvfvrneq  5761  fliftfun  5775  isotr  5795  isoini  5797  isopolem  5801  isosolem  5803  moriotass  5837  acexmidlem2  5850  suppssfv  6057  suppssov1  6058  f1dmex  6095  releldm2  6164  f1o2ndf1  6207  poxp  6211  tposf2  6247  iunon  6263  smoel2  6282  tfrlem9  6298  tfrexlem  6313  tfr1onlembxssdm  6322  tfr1onlemres  6328  tfrcllembxssdm  6335  tfrcllemres  6341  tfrcl  6343  tfri3  6346  frecabcl  6378  sucinc2  6425  nnacom  6463  nnmcom  6468  nnsucsssuc  6471  nnsucuniel  6474  nntri2or2  6477  nnaordi  6487  nnmordi  6495  nnaordex  6507  nnm00  6509  ectocld  6579  iinerm  6585  th3qlem2  6616  elpm2r  6644  mapsncnv  6673  mptelixpg  6712  ixpsnf1o  6714  f1oen3g  6732  f1oeng  6735  en2d  6746  en3d  6747  dom2lem  6750  fundmen  6784  fundmeng  6785  unen  6794  xpdom2  6809  xpdom2g  6810  fopwdom  6814  nneneq  6835  phpm  6843  phpelm  6844  dif1enen  6858  fin0  6863  findcard  6866  diffifi  6872  ac6sfi  6876  onunsnss  6894  fiintim  6906  xpfi  6907  fidcenum  6933  sbthlem1  6934  sbthlemi3  6936  sbthlemi10  6943  elfir  6950  isotilem  6983  inflbti  7001  ordiso2  7012  eldju2ndl  7049  eldju2ndr  7050  updjudhf  7056  mkvprop  7134  carden2bex  7166  pm54.43  7167  exmidfodomrlemeldju  7176  exmidfodomrlemreseldju  7177  exmidfodomrlemim  7178  ltmpig  7301  enq0sym  7394  addnq0mo  7409  mulnq0mo  7410  prarloclem3step  7458  prarloclem3  7459  genpml  7479  genpmu  7480  genprndl  7483  genprndu  7484  genpdisj  7485  distrlem1prl  7544  distrlem1pru  7545  distrlem4prl  7546  distrlem4pru  7547  distrlem5prl  7548  distrlem5pru  7549  ltsopr  7558  ltaddpr  7559  addcanprleml  7576  addcanprlemu  7577  recexprlemm  7586  recexprlemlol  7588  recexprlemupu  7590  aptiprleml  7601  aptiprlemu  7602  caucvgprlemnkj  7628  caucvgprlemnbj  7629  addsrmo  7705  mulsrmo  7706  srpospr  7745  caucvgsr  7764  axprecex  7842  mulgt0  7994  ltne  8004  cnegexlem1  8094  cnegexlem2  8095  negf1o  8301  addgt0  8367  addgegt0  8368  addgtge0  8369  addge0  8370  recexre  8497  mulge0  8538  recexap  8571  prodgt02  8769  prodge02  8771  ltmul12a  8776  mulgt1  8779  nndivtr  8920  addltmul  9114  elnnnn0b  9179  xnn0nnn0pnf  9211  elnnz  9222  zmulcl  9265  nn0n0n1ge2  9282  nn0lt2  9293  nn0le2is012  9294  uzind2  9324  nn0ind-raph  9329  eluzp1m1  9510  uz3m2nn  9532  supinfneg  9554  infsupneg  9555  infregelbex  9557  negm  9574  lbzbi  9575  qaddcl  9594  qmulcl  9596  qreccl  9601  elpq  9607  ledivge1le  9683  nn0ledivnn  9724  xrltne  9770  xrre  9777  xrre2  9778  xrre3  9779  ge0gtmnf  9780  xltnegi  9792  xnn0xadd0  9824  xnegdi  9825  xposdif  9839  xlesubadd  9840  iccsupr  9923  icoshft  9947  icoshftf1o  9948  fznlem  9997  fzen  9999  uzsubsubfz  10003  fzsuc2  10035  elfz1b  10046  elfz0ubfz0  10081  elfz0fzfz0  10082  fz0fzelfz0  10083  fz0fzdiffz0  10086  elfzmlbp  10088  difelfznle  10091  fzofzim  10144  eluzgtdifelfzo  10153  elfzodifsumelfzo  10157  elfzonlteqm1  10166  elfzom1p1elfzo  10170  ssfzo12bi  10181  subfzo0  10198  exbtwnzlemstep  10204  modqmuladdnn0  10324  modfzo0difsn  10351  addmodlteq  10354  frec2uzlt2d  10360  frecuzrdgtcl  10368  frecuzrdgfunlem  10375  m1expcl2  10498  expge1  10513  leexp2r  10530  expubnd  10533  zesq  10594  expnlbnd  10600  nn0ltexp2  10644  nn0opthd  10656  faclbnd  10675  bcpasc  10700  hashprg  10743  seq3coll  10777  rexanuz  10952  rexuz3  10954  r19.29uz  10956  r19.2uz  10957  absnid  11037  leabs  11038  ltabs  11051  icodiamlt  11144  maxleast  11177  negfi  11191  climcn2  11272  climcau  11310  climcaucn  11314  sumdc  11321  fsum3cvg  11341  isumz  11352  fsumf1o  11353  fisumss  11355  isumss2  11356  fsumzcl2  11368  fsumsplit  11370  fsumsplitsnun  11382  sumsplitdc  11395  fsum2dlemstep  11397  telfsumo  11429  fsumparts  11433  fsumiun  11440  isumrpcl  11457  fproddccvg  11535  prod1dc  11549  prodssdc  11552  fprodssdc  11553  prodsnf  11555  fprodsplitdc  11559  fprod2dlemstep  11585  fprodmodd  11604  efexp  11645  efieq1re  11734  p1modz1  11756  dvds0lem  11763  dvds2ln  11786  dvdssub2  11797  dvdsadd2b  11802  dvdsabseq  11807  divconjdvds  11809  dvdsdivcl  11810  odd2np1  11832  oddge22np1  11840  opoe  11854  omoe  11855  opeo  11856  omeo  11857  m1expo  11859  nn0ehalf  11862  nn0o1gt2  11864  nno  11865  divalgb  11884  ndvdsadd  11890  zsupcllemex  11901  zssinfcl  11903  gcd0id  11934  gcdneg  11937  gcdaddm  11939  bezoutlemstep  11952  dfgcd2  11969  gcddiv  11974  dvdsmulgcd  11980  bezoutr  11987  bezoutr1  11988  uzwodc  11992  algfx  12006  lcmgcdlem  12031  lcmgcdeq  12037  coprmdvds  12046  divgcdcoprmex  12056  cncongr1  12057  cncongr2  12058  isprm3  12072  dvdsnprmd  12079  prmgt1  12086  oddprmgt2  12088  isprm6  12101  cncongrprm  12111  phibndlem  12170  phimullem  12179  powm2modprm  12206  modprm0  12208  modprmn0modprm0  12210  prm23lt5  12217  pcneg  12278  pcprmpw2  12286  dvdsprmpweqnn  12289  dvdsprmpweqle  12290  pcaddlem  12292  fldivp1  12300  pcfac  12302  oddprmdvds  12306  prmunb  12314  ennnfone  12380  unct  12397  lidrididd  12636  sgrpass  12649  mnd1id  12680  insubm  12703  dfgrp2  12732  grpid  12742  grpasscan1  12762  uniopn  12793  istopon  12805  fiinbas  12841  tg2  12854  tgcl  12858  0nnei  12947  tgrest  12963  tgcn  13002  cnpnei  13013  cncnp2m  13025  lmtopcnp  13044  tx2cn  13064  txcn  13069  cnmpt21  13085  isxmet2d  13142  metrest  13300  metcnpi3  13311  tgioo  13340  fsumcncntop  13350  elcncf1di  13360  climcncf  13365  cncfco  13372  suplociccreex  13396  cnplimcim  13430  cnlimci  13436  reeff1olem  13486  efltlemlt  13489  zabsle1  13694  lgslem3  13697  lgsmod  13721  lgsdir2lem5  13727  lgsdir2  13728  lgsne0  13733  lgsdirnn0  13742  bj-charfun  13842  bj-charfunr  13845  bj-charfunbi  13846  bj-prexg  13946  peano5set  13975  bj-peano4  13990  bj-nn0suc  13999  bj-nn0sucALT  14013  bj-findis  14014  exmidsbthrlem  14054  trilpolemres  14074  trirec0  14076  nconstwlpolem  14096  neapmkv  14099