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	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
imp	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Proof of Theorem imp

Step	Hyp	Ref	Expression
1		simpl 109	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜑)
2		simpr 110	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜓)
3		imp.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	1, 2, 3	sylc 62	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)

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  602  pm3.43  604  con3dimp  638  annimim  690  imnan  694  jaoian  800  jaodan  802  stdcndc  850  impidc  863  pm2.5gdc  871  con2bidc  880  pm5.18dc  888  dfandc  889  pm4.63dc  891  pm4.54dc  907  pm4.79dc  908  orcanai  933  annimdc  943  pm4.55dc  944  orandc  945  pm4.82  956  pm3.11dc  963  pm3.12dc  964  dn1dc  966  3jcad  1202  3expia  1229  3an1rs  1243  3imp1  1244  3imp2  1246  syl3anl2  1320  3jaoian  1339  3jaodan  1340  mp3anl1  1365  mp3anl2  1366  mp3anl3  1367  ecased  1383  xor3dc  1429  pm5.15dc  1431  xor2dc  1432  xornbidc  1433  xordc  1434  nbbndc  1436  biassdc  1437  bilukdc  1438  dfbi3dc  1439  pm5.24dc  1440  xordidc  1441  alanimi  1505  19.29  1666  equs4  1771  equsexd  1775  spimth  1781  equs5a  1840  ax11v2  1866  ax11b  1872  equs5or  1876  sb5rf  1898  equvin  1909  nfsb4t  2065  eu5  2125  mopick  2156  euexex  2163  2euswapdc  2169  exists2  2175  eqrdav  2228  dvelimdc  2393  nebidc  2480  pm13.18  2481  nelne1  2490  nelne2  2491  rspa  2578  ralrimdvv  2614  r19.21bi  2618  r19.26  2657  ralbi  2663  rexbi  2664  r19.29  2668  vtoclgft  2852  rspcva  2906  rspc2va  2922  elabgt  2945  eqeu  2974  mob2  2984  mob  2986  euind  2991  reu6  2993  reuind  3009  sbctt  3096  rspsbca  3114  sbcnestgf  3177  rspcsbela  3185  ssel2  3220  sselda  3225  sstr  3233  nssne1  3283  nssne2  3284  reuss2  3485  reupick  3489  reupick2  3491  reximdva0m  3508  ssn0  3535  disjel  3547  ssdisj  3549  absneu  3741  preqr1g  3847  prel12  3852  dfiun2g  4000  nbrne1  4105  nbrne2  4106  mpteq12f  4167  triun  4198  csbexga  4215  prcssprc  4228  iinexgm  4242  prexg  4299  copsex2t  4335  swopo  4401  poirr  4402  potr  4403  pofun  4407  issod  4414  ordelss  4474  trssord  4475  limelon  4494  trsuc  4517  eusvnfb  4549  rabxfrd  4564  regexmidlem1  4629  nordeq  4640  suc11g  4653  nnsuc  4712  brrelex12  4762  vtoclr  4772  optocl  4800  relop  4878  brcogw  4897  breldmg  4935  elreldm  4956  riinint  4991  issref  5117  xpidtr  5125  trin2  5126  cnveqb  5190  funopg  5358  funssres  5366  fununi  5395  funimass2  5405  imain  5409  fnun  5435  fco  5497  opelf  5504  f0rn0  5528  f1oun  5600  fun11iun  5601  fv3  5658  ndmfvg  5666  fvelima  5693  fvopab3ig  5716  fvmptssdm  5727  fvmptf  5735  fvimacnv  5758  fmptco  5809  fcof  5828  funfvima2  5882  funfvima3  5883  f1veqaeq  5905  f1ocnvfvrneq  5918  fliftfun  5932  isotr  5952  isoini  5954  isopolem  5958  isosolem  5960  moriotass  5997  acexmidlem2  6010  suppssfv  6226  suppssov1  6227  f1dmex  6273  releldm2  6343  f1o2ndf1  6388  poxp  6392  tposf2  6429  iunon  6445  smoel2  6464  tfrlem9  6480  tfrexlem  6495  tfr1onlembxssdm  6504  tfr1onlemres  6510  tfrcllembxssdm  6517  tfrcllemres  6523  tfrcl  6525  tfri3  6528  frecabcl  6560  sucinc2  6609  nnacom  6647  nnmcom  6652  nnsucsssuc  6655  nnsucuniel  6658  nntri2or2  6661  nnaordi  6671  nnmordi  6679  nnaordex  6691  nnm00  6693  ectocld  6765  iinerm  6771  th3qlem2  6802  elpm2r  6830  mapsncnv  6859  mptelixpg  6898  ixpsnf1o  6900  f1oen4g  6920  f1dom4g  6921  f1oen3g  6922  f1oeng  6925  en2d  6936  en3d  6937  dom2lem  6940  fundmen  6976  fundmeng  6977  unen  6986  modom  6989  rex2dom  6991  en2m  6994  xpdom2  7010  xpdom2g  7011  fopwdom  7017  nneneq  7038  phpm  7047  phpelm  7048  dif1enen  7064  fin0  7069  findcard  7072  diffifi  7078  ac6sfi  7082  onunsnss  7104  fiintim  7118  xpfi  7119  infidc  7127  fidcenum  7149  sbthlem1  7150  sbthlemi3  7152  sbthlemi10  7159  elfir  7166  isotilem  7199  inflbti  7217  ordiso2  7228  eldju2ndl  7265  eldju2ndr  7266  updjudhf  7272  mkvprop  7351  carden2bex  7388  pm54.43  7389  exmidfodomrlemeldju  7403  exmidfodomrlemreseldju  7404  exmidfodomrlemim  7405  pw1m  7435  ltmpig  7552  enq0sym  7645  addnq0mo  7660  mulnq0mo  7661  prarloclem3step  7709  prarloclem3  7710  genpml  7730  genpmu  7731  genprndl  7734  genprndu  7735  genpdisj  7736  distrlem1prl  7795  distrlem1pru  7796  distrlem4prl  7797  distrlem4pru  7798  distrlem5prl  7799  distrlem5pru  7800  ltsopr  7809  ltaddpr  7810  addcanprleml  7827  addcanprlemu  7828  recexprlemm  7837  recexprlemlol  7839  recexprlemupu  7841  aptiprleml  7852  aptiprlemu  7853  caucvgprlemnkj  7879  caucvgprlemnbj  7880  addsrmo  7956  mulsrmo  7957  srpospr  7996  caucvgsr  8015  axprecex  8093  mpomulf  8162  mulgt0  8247  ltne  8257  cnegexlem1  8347  cnegexlem2  8348  negf1o  8554  addgt0  8621  addgegt0  8622  addgtge0  8623  addge0  8624  recexre  8751  mulge0  8792  recexap  8826  prodgt02  9026  prodge02  9028  ltmul12a  9033  mulgt1  9036  nndivtr  9178  addltmul  9374  elnnnn0b  9439  xnn0nnn0pnf  9471  elnnz  9482  zmulcl  9526  nn0n0n1ge2  9543  nn0lt2  9554  nn0le2is012  9555  uzind2  9585  nn0ind-raph  9590  eluzp1m1  9773  uz3m2nn  9800  supinfneg  9822  infsupneg  9823  infregelbex  9825  negm  9842  lbzbi  9843  qaddcl  9862  qmulcl  9864  qreccl  9869  elpq  9876  ledivge1le  9954  nn0ledivnn  9995  xrltne  10041  xrre  10048  xrre2  10049  xrre3  10050  ge0gtmnf  10051  xltnegi  10063  xnn0xadd0  10095  xnegdi  10096  xposdif  10110  xlesubadd  10111  iccsupr  10194  icoshft  10218  icoshftf1o  10219  fznlem  10269  fzen  10271  uzsubsubfz  10275  fzsuc2  10307  elfz1b  10318  elfz0ubfz0  10353  elfz0fzfz0  10354  fz0fzelfz0  10355  fz0fzdiffz0  10358  elfzmlbp  10360  difelfznle  10363  fzofzim  10420  elincfzoext  10431  eluzgtdifelfzo  10435  elfzodifsumelfzo  10439  elfzonlteqm1  10448  elfzom1p1elfzo  10452  ssfzo12bi  10463  subfzo0  10481  zsupcllemex  10483  zssinfcl  10485  exbtwnzlemstep  10500  modqmuladdnn0  10623  modfzo0difsn  10650  addmodlteq  10653  frec2uzlt2d  10659  frecuzrdgtcl  10667  frecuzrdgfunlem  10674  seqf1og  10776  m1expcl2  10816  expge1  10831  leexp2r  10848  expubnd  10851  zesq  10913  expnlbnd  10919  nn0ltexp2  10964  nn0opthd  10977  faclbnd  10996  bcpasc  11021  hashprg  11065  seq3coll  11099  wrdnval  11137  wrdsymb0  11139  fstwrdne  11145  wrdred1hash  11150  swrdnd  11233  swrdwrdsymbg  11238  swrdsbslen  11240  swrdlsw  11243  swrdswrdlem  11278  swrdswrd  11279  pfxswrd  11280  cats1un  11295  wrd2ind  11297  swrdccatin1  11299  pfxccatin12lem4  11300  pfxccatin12lem2a  11301  pfxccatin12lem1  11302  swrdccatin2  11303  pfxccatin12lem2c  11304  pfxccatin12lem2  11305  pfxccatin12lem3  11306  pfxccatin12  11307  pfxccat3  11308  swrdccat  11309  pfxccat3a  11312  swrdccat3blem  11313  swrdccat3b  11314  swrdccatin2d  11318  reuccatpfxs1lem  11320  rexanuz  11542  rexuz3  11544  r19.29uz  11546  r19.2uz  11547  absnid  11627  leabs  11628  ltabs  11641  icodiamlt  11734  maxleast  11767  negfi  11782  climcn2  11863  climcau  11901  climcaucn  11905  sumdc  11912  fsum3cvg  11932  isumz  11943  fsumf1o  11944  fisumss  11946  isumss2  11947  fsumzcl2  11959  fsumsplit  11961  fsumsplitsnun  11973  sumsplitdc  11986  fsum2dlemstep  11988  telfsumo  12020  fsumparts  12024  fsumiun  12031  isumrpcl  12048  fproddccvg  12126  prod1dc  12140  prodssdc  12143  fprodssdc  12144  prodsnf  12146  fprodsplitdc  12150  fprod2dlemstep  12176  fprodmodd  12195  efexp  12236  efieq1re  12326  p1modz1  12348  dvds0lem  12355  dvds2ln  12378  dvdssub2  12389  dvdsadd2b  12394  dvdsabseq  12401  divconjdvds  12403  dvdsdivcl  12404  odd2np1  12427  oddge22np1  12435  opoe  12449  omoe  12450  opeo  12451  omeo  12452  m1expo  12454  nn0ehalf  12457  nn0o1gt2  12459  nno  12460  divalgb  12479  ndvdsadd  12485  bitsinv1lem  12515  gcd0id  12543  gcdneg  12546  gcdaddm  12548  bezoutlemstep  12561  dfgcd2  12578  gcddiv  12583  dvdsmulgcd  12589  bezoutr  12596  bezoutr1  12597  uzwodc  12601  nninfctlemfo  12604  algfx  12617  lcmgcdlem  12642  lcmgcdeq  12648  coprmdvds  12657  divgcdcoprmex  12667  cncongr1  12668  cncongr2  12669  isprm3  12683  dvdsnprmd  12690  prmgt1  12697  oddprmgt2  12699  isprm6  12712  cncongrprm  12722  phibndlem  12781  phimullem  12790  powm2modprm  12818  modprm0  12820  modprmn0modprm0  12822  prm23lt5  12829  pcneg  12891  pcprmpw2  12899  dvdsprmpweqnn  12902  dvdsprmpweqle  12903  pcaddlem  12905  fldivp1  12914  pcfac  12916  oddprmdvds  12920  prmunb  12928  ennnfone  13039  unct  13056  lidrididd  13458  gsummgmpropd  13470  sgrpass  13484  issgrpd  13488  issubmnd  13518  imasmnd2  13528  mnd1id  13532  insubm  13561  dfgrp2  13603  grpid  13615  grpasscan1  13639  dfgrp3mlem  13674  dfgrp3me  13676  imasgrp2  13690  mulgnn0gsum  13708  mulgnn0p1  13713  mulgaddcom  13726  mulginvcom  13727  mulgass  13739  mulgpropdg  13744  subginv  13761  issubg2m  13769  issubg4m  13773  grpissubg  13774  resgrpisgrp  13775  subgintm  13778  kerf1ghm  13854  cmncom  13882  imasabl  13916  rngdi  13946  rngdir  13947  rngpropd  13961  imasrng  13962  imasring  14070  nzrunit  14195  issubrng2  14217  subrngintm  14219  issubrg2  14248  subrgintm  14250  lmodfopnelem1  14331  lmodfopnelem2  14332  lmodfopne  14333  islssm  14364  islidlm  14486  rnglidlmcl  14487  dflidl2rng  14488  rnglidlmmgm  14503  rnglidlmsgrp  14504  rnglidlrng  14505  dvdsrzring  14610  znidom  14664  uniopn  14718  istopon  14730  fiinbas  14766  tg2  14777  tgcl  14781  0nnei  14870  tgrest  14886  tgcn  14925  cnpnei  14936  cncnp2m  14948  lmtopcnp  14967  tx2cn  14987  txcn  14992  cnmpt21  15008  isxmet2d  15065  metrest  15223  metcnpi3  15234  tgioo  15271  fsumcncntop  15284  elcncf1di  15296  climcncf  15301  cncfco  15308  suplociccreex  15341  cnplimcim  15384  cnlimci  15390  reeff1olem  15488  efltlemlt  15491  zabsle1  15721  lgslem3  15724  lgsmod  15748  lgsdir2lem5  15754  lgsdir2  15755  lgsne0  15760  lgsdirnn0  15769  gausslemma2dlem0f  15776  gausslemma2dlem1a  15780  gausslemma2dlem3  15785  2lgslem1c  15812  2lgslem3a1  15819  2lgslem3b1  15820  2lgslem3c1  15821  2lgslem3d1  15822  2lgslem3  15823  2lgsoddprmlem2  15828  uhgrm  15922  incistruhgr  15934  upgrfnen  15942  umgrfnen  15952  umgrnloop  15960  upgredgpr  15993  usgrausgrben  16016  usgredgop  16017  usgruspgrben  16030  usgrislfuspgrdom  16034  umgrvad2edg  16055  ushgredgedg  16070  ushgredgedgloop  16072  uhgr0v0e  16078  vtxdg0v  16105  wlkpropg  16135  wlkvg  16139  wlkl1loop  16169  upgriswlkdc  16171  upgrwlkedg  16172  upgrwlkvtxedg  16175  uspgr2wlkeq  16176  wlkres  16188  trlf1  16197  clwwlk1loop  16208  clwwlkccatlem  16209  isclwwlknx  16225  clwwlkn1loopb  16229  clwwlkext2edg  16231  umgr2cwwk2dif  16233  clwwlknonex2lem2  16247  clwwlknonex2  16248  eupthseg  16261  bj-charfun  16352  bj-charfunr  16355  bj-charfunbi  16356  bj-prexg  16456  peano5set  16485  bj-peano4  16500  bj-nn0suc  16509  bj-nn0sucALT  16523  bj-findis  16524  exmidsbthrlem  16576  trilpolemres  16596  trirec0  16598  nconstwlpolem  16619  neapmkv  16622  gfsumval  16630