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  560  anabsi5  581  anim12dan  604  pm3.43  606  con3dimp  640  annimim  693  imnan  697  jaoian  803  jaodan  805  stdcndc  853  impidc  866  pm2.5gdc  874  con2bidc  883  pm5.18dc  891  dfandc  892  pm4.63dc  894  pm4.54dc  910  pm4.79dc  911  orcanai  936  annimdc  946  pm4.55dc  947  orandc  948  pm4.82  959  pm3.11dc  966  pm3.12dc  967  dn1dc  969  3jcad  1205  3expia  1232  3an1rs  1246  3imp1  1247  3imp2  1249  syl3anl2  1323  3jaoian  1342  3jaodan  1343  mp3anl1  1368  mp3anl2  1369  mp3anl3  1370  ecased  1386  xor3dc  1432  pm5.15dc  1434  xor2dc  1435  xornbidc  1436  xordc  1437  nbbndc  1439  biassdc  1440  bilukdc  1441  dfbi3dc  1442  pm5.24dc  1443  xordidc  1444  alanimi  1508  19.29  1669  equs4  1773  equsexd  1778  spimth  1784  equs5a  1843  ax11v2  1869  ax11b  1875  equs5or  1879  sb5rf  1901  equvin  1912  nfsb4t  2070  eu5  2130  mopick  2161  euexex  2168  2euswapdc  2174  exists2  2180  eqrdav  2233  dvelimdc  2407  nebidc  2494  pm13.18  2495  nelne1  2504  nelne2  2505  rspa  2592  ralrimdvv  2628  r19.21bi  2632  r19.26  2671  ralbi  2677  rexbi  2678  r19.29  2682  vtoclgft  2867  rspcva  2921  rspc2va  2937  elabgt  2960  eqeu  2989  mob2  2999  mob  3001  euind  3006  reu6  3008  reuind  3024  sbctt  3111  rspsbca  3129  sbcnestgf  3192  rspcsbela  3200  ssel2  3235  sselda  3240  sstr  3248  nssne1  3298  nssne2  3299  reuss2  3503  reupick  3507  reupick2  3509  reximdva0m  3526  ssn0  3553  disjel  3565  ssdisj  3567  absneu  3765  preqr1g  3872  prel12  3877  dfiun2g  4025  nbrne1  4130  nbrne2  4131  mpteq12f  4192  triun  4223  csbexga  4240  prcssprc  4253  iinexgm  4268  prexg  4327  copsex2t  4363  swopo  4429  poirr  4430  potr  4431  pofun  4435  issod  4442  ordelss  4502  trssord  4503  limelon  4522  trsuc  4545  eusvnfb  4577  rabxfrd  4592  regexmidlem1  4657  nordeq  4668  suc11g  4681  nnsuc  4740  brrelex12  4790  vtoclr  4800  optocl  4828  relop  4907  brcogw  4926  breldmg  4964  elreldm  4985  riinint  5020  xpexcnvm  5119  issref  5147  xpidtr  5155  trin2  5156  cnveqb  5220  funopg  5388  funssres  5397  fununi  5426  funimass2  5436  imain  5440  fnun  5466  fco  5529  opelf  5537  f0rn0  5564  f1oun  5636  fun11iun  5637  fv3  5695  ndmfvg  5703  fvelima  5730  fvopab3ig  5753  fvmptssdm  5764  fvmptf  5772  fvimacnv  5795  fmptco  5845  fcof  5865  funfvima2  5921  funfvima3  5922  f1veqaeq  5944  f1ocnvfvrneq  5957  fliftfun  5971  isotr  5991  isoini  5993  isopolem  5997  isosolem  5999  moriotass  6036  acexmidlem2  6049  suppssov1  6265  f1dmex  6311  releldm2  6381  f1o2ndf1  6426  poxp  6430  fsuppeq  6449  suppssfvg  6465  tposf2  6501  iunon  6517  smoel2  6536  tfrlem9  6552  tfrexlem  6567  tfr1onlembxssdm  6576  tfr1onlemres  6582  tfrcllembxssdm  6589  tfrcllemres  6595  tfrcl  6597  tfri3  6600  frecabcl  6632  sucinc2  6681  nnacom  6719  nnmcom  6724  nnsucsssuc  6727  nnsucuniel  6730  nntri2or2  6733  nnaordi  6743  nnmordi  6751  nnaordex  6763  nnm00  6765  ectocld  6837  iinerm  6843  th3qlem2  6874  elpm2r  6902  mapsnd  6925  mapsncnv  6932  mptelixpg  6971  ixpsnf1o  6973  f1oen4g  6993  f1dom4g  6994  f1oen3g  6995  f1oeng  6998  en2d  7009  en3d  7010  dom2lem  7013  fundmen  7049  fundmeng  7050  unen  7060  modom  7063  rex2dom  7065  en2m  7068  xpdom2  7084  xpdom2g  7085  fopwdom  7091  nneneq  7113  phpm  7122  phpelm  7123  dif1enen  7139  fin0  7144  findcard  7147  diffifi  7153  ac6sfi  7157  onunsnss  7179  fiintim  7193  xpfi  7194  infidc  7203  fidcenum  7228  sbthlem1  7229  sbthlemi3  7231  sbthlemi10  7238  ffsuppbi  7255  elfir  7262  isotilem  7299  inflbti  7317  ordiso2  7328  eldju2ndl  7365  eldju2ndr  7366  updjudhf  7372  mkvprop  7451  carden2bex  7488  pm54.43  7489  exmidfodomrlemeldju  7504  exmidfodomrlemreseldju  7505  exmidfodomrlemim  7506  pw1m  7536  ltmpig  7659  enq0sym  7752  addnq0mo  7767  mulnq0mo  7768  prarloclem3step  7816  prarloclem3  7817  genpml  7837  genpmu  7838  genprndl  7841  genprndu  7842  genpdisj  7843  distrlem1prl  7902  distrlem1pru  7903  distrlem4prl  7904  distrlem4pru  7905  distrlem5prl  7906  distrlem5pru  7907  ltsopr  7916  ltaddpr  7917  addcanprleml  7934  addcanprlemu  7935  recexprlemm  7944  recexprlemlol  7946  recexprlemupu  7948  aptiprleml  7959  aptiprlemu  7960  caucvgprlemnkj  7986  caucvgprlemnbj  7987  addsrmo  8063  mulsrmo  8064  srpospr  8103  caucvgsr  8122  axprecex  8200  mpomulf  8269  mulgt0  8353  ltne  8363  cnegexlem1  8453  cnegexlem2  8454  negf1o  8660  addgt0  8727  addgegt0  8728  addgtge0  8729  addge0  8730  recexre  8857  mulge0  8898  recexap  8932  prodgt02  9132  prodge02  9134  ltmul12a  9139  mulgt1  9142  nndivtr  9284  addltmul  9480  elnnnn0b  9545  fcdmnn0supp  9553  fcdmnn0fsupp  9554  fcdmnn0suppg  9555  xnn0nnn0pnf  9581  elnnz  9592  zmulcl  9636  nn0n0n1ge2  9653  nn0lt2  9665  nn0le2is012  9666  uzind2  9696  nn0ind-raph  9701  eluzp1m1  9884  uz3m2nn  9911  supinfneg  9933  infsupneg  9934  infregelbex  9936  negm  9953  lbzbi  9954  qaddcl  9973  qmulcl  9975  qreccl  9980  elpq  9987  ledivge1le  10065  nn0ledivnn  10106  xrltne  10152  xrre  10159  xrre2  10160  xrre3  10161  ge0gtmnf  10162  xltnegi  10174  xnn0xadd0  10206  xnegdi  10207  xposdif  10221  xlesubadd  10222  iccsupr  10305  icoshft  10329  icoshftf1o  10330  fznlem  10381  fzen  10383  uzsubsubfz  10387  fzsuc2  10420  elfz1b  10431  elfz0ubfz0  10466  elfz0fzfz0  10467  fz0fzelfz0  10468  fz0fzdiffz0  10471  elfzmlbp  10473  difelfznle  10476  nn0p1elfzo  10528  fzofzim  10534  elincfzoext  10545  eluzgtdifelfzo  10549  elfzodifsumelfzo  10553  elfzonlteqm1  10562  elfzom1p1elfzo  10566  ssfzo12bi  10577  subfzo0  10595  zsupcllemex  10597  zssinfcl  10599  exbtwnzlemstep  10614  modqmuladdnn0  10737  modfzo0difsn  10764  addmodlteq  10767  frec2uzlt2d  10773  frecuzrdgtcl  10781  frecuzrdgfunlem  10788  seqf1og  10890  m1expcl2  10930  expge1  10945  leexp2r  10962  expubnd  10965  zesq  11028  expnlbnd  11034  nn0ltexp2  11079  nn0opthd  11092  faclbnd  11111  bcpasc  11136  hashprg  11181  seq3coll  11222  wrdnval  11263  wrdsymb0  11265  fstwrdne  11271  wrdred1hash  11276  swrdnd  11359  swrdwrdsymbg  11364  swrdsbslen  11366  swrdlsw  11369  swrdswrdlem  11404  swrdswrd  11405  pfxswrd  11406  cats1un  11421  wrd2ind  11423  swrdccatin1  11425  pfxccatin12lem4  11426  pfxccatin12lem2a  11427  pfxccatin12lem1  11428  swrdccatin2  11429  pfxccatin12lem2c  11430  pfxccatin12lem2  11431  pfxccatin12lem3  11432  pfxccatin12  11433  pfxccat3  11434  swrdccat  11435  pfxccat3a  11438  swrdccat3blem  11439  swrdccat3b  11440  swrdccatin2d  11444  reuccatpfxs1lem  11446  rexanuz  11681  rexuz3  11683  r19.29uz  11685  r19.2uz  11686  absnid  11766  leabs  11767  ltabs  11780  icodiamlt  11873  maxleast  11906  negfi  11921  climcn2  12002  climcau  12040  climcaucn  12044  sumdc  12051  fsum3cvg  12072  isumz  12083  fsumf1o  12084  fisumss  12086  isumss2  12087  fsumzcl2  12099  fsumsplit  12101  fsumsplitsnun  12113  sumsplitdc  12126  fsum2dlemstep  12128  telfsumo  12160  fsumparts  12164  fsumiun  12171  isumrpcl  12188  fproddccvg  12266  prod1dc  12280  prodssdc  12283  fprodssdc  12284  prodsnf  12286  fprodsplitdc  12290  fprod2dlemstep  12316  fprodmodd  12335  efexp  12376  efieq1re  12466  p1modz1  12488  dvds0lem  12495  dvds2ln  12518  dvdssub2  12529  dvdsadd2b  12534  dvdsabseq  12541  divconjdvds  12543  dvdsdivcl  12544  odd2np1  12567  oddge22np1  12575  opoe  12589  omoe  12590  opeo  12591  omeo  12592  m1expo  12594  nn0ehalf  12597  nn0o1gt2  12599  nno  12600  divalgb  12619  ndvdsadd  12625  bitsinv1lem  12655  gcd0id  12683  gcdneg  12686  gcdaddm  12688  bezoutlemstep  12701  dfgcd2  12718  gcddiv  12723  dvdsmulgcd  12729  bezoutr  12736  bezoutr1  12737  uzwodc  12741  nninfctlemfo  12744  algfx  12757  lcmgcdlem  12782  lcmgcdeq  12788  coprmdvds  12797  divgcdcoprmex  12807  cncongr1  12808  cncongr2  12809  isprm3  12823  dvdsnprmd  12830  prmgt1  12837  oddprmgt2  12839  isprm6  12852  cncongrprm  12862  phibndlem  12921  phimullem  12930  powm2modprm  12958  modprm0  12960  modprmn0modprm0  12962  prm23lt5  12969  pcneg  13031  pcprmpw2  13039  dvdsprmpweqnn  13042  dvdsprmpweqle  13043  pcaddlem  13045  fldivp1  13054  pcfac  13056  oddprmdvds  13060  prmunb  13068  ballotfilemfc0  13157  ballotfilemfcc  13158  ballotfilem4  13163  ennnfone  13197  unct  13214  lidrididd  13616  gsummgmpropd  13628  sgrpass  13642  issgrpd  13646  issubmnd  13676  imasmnd2  13686  mnd1id  13690  insubm  13719  dfgrp2  13761  grpid  13773  grpasscan1  13797  dfgrp3mlem  13832  dfgrp3me  13834  imasgrp2  13848  mulgnn0gsum  13866  mulgnn0p1  13871  mulgaddcom  13884  mulginvcom  13885  mulgass  13897  mulgpropdg  13902  subginv  13919  issubg2m  13927  issubg4m  13931  grpissubg  13932  resgrpisgrp  13933  subgintm  13936  kerf1ghm  14012  cmncom  14040  imasabl  14074  rngdi  14105  rngdir  14106  rngpropd  14120  imasrng  14121  imasring  14229  nzrunit  14355  issubrng2  14378  subrngintm  14380  issubrg2  14409  subrgintm  14411  lmodfopnelem1  14521  lmodfopnelem2  14522  lmodfopne  14523  islssm  14554  islidlm  14676  rnglidlmcl  14677  dflidl2rng  14678  rnglidlmmgm  14693  rnglidlmsgrp  14694  rnglidlrng  14695  dvdsrzring  14800  znidom  14854  uniopn  14915  istopon  14927  fiinbas  14963  tg2  14974  tgcl  14978  0nnei  15067  tgrest  15083  tgcn  15122  cnpnei  15133  cncnp2m  15145  lmtopcnp  15164  tx2cn  15184  txcn  15189  cnmpt21  15205  isxmet2d  15262  metrest  15420  metcnpi3  15431  tgioo  15468  fsumcncntop  15481  elcncf1di  15493  climcncf  15498  cncfco  15505  suplociccreex  15538  cnplimcim  15581  cnlimci  15587  reeff1olem  15685  efltlemlt  15688  pellexlem1  15894  zabsle1  15921  lgslem3  15924  lgsmod  15948  lgsdir2lem5  15954  lgsdir2  15955  lgsne0  15960  lgsdirnn0  15969  gausslemma2dlem0f  15976  gausslemma2dlem1a  15980  gausslemma2dlem3  15985  2lgslem1c  16012  2lgslem3a1  16019  2lgslem3b1  16020  2lgslem3c1  16021  2lgslem3d1  16022  2lgslem3  16023  2lgsoddprmlem2  16028  uhgrm  16122  incistruhgr  16134  upgrfnen  16142  umgrfnen  16152  umgrnloop  16160  upgredgpr  16193  usgrausgrben  16216  usgredgop  16217  usgruspgrben  16230  usgrislfuspgrdom  16234  umgrvad2edg  16255  ushgredgedg  16270  ushgredgedgloop  16272  uhgr0v0e  16278  subgreldmiedg  16313  subupgr  16317  uhgrspansubgrlem  16320  vtxdg0v  16338  wlkpropg  16368  wlkvg  16372  wlkl1loop  16402  upgriswlkdc  16404  upgrwlkedg  16405  upgrwlkvtxedg  16408  uspgr2wlkeq  16409  wlkres  16423  trlf1  16432  clwwlk1loop  16443  clwwlkccatlem  16444  isclwwlknx  16460  clwwlkn1loopb  16464  clwwlkext2edg  16466  umgr2cwwk2dif  16468  clwwlknonex2lem2  16482  clwwlknonex2  16483  eupthseg  16496  eupth2lem3lem4fi  16517  bj-charfun  16626  bj-charfunr  16629  bj-charfunbi  16630  bj-prexg  16730  peano5set  16759  bj-peano4  16774  bj-nn0suc  16783  bj-nn0sucALT  16797  bj-findis  16798  exmidsbthrlem  16851  trilpolemres  16875  trirec0  16877  nconstwlpolem  16900  neapmkv  16903  gfsumval  16911