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  413  sylan9r  414  imdistani  449  mpan10  478  adantl4r  521  adantl5r  529  adantl6r  530  a2and  564  anabsi5  585  anim12dan  608  pm3.43  610  con3dimp  644  annimim  697  imnan  701  jaoian  807  jaodan  809  stdcndc  857  impidc  870  pm2.5gdc  878  con2bidc  887  pm5.18dc  895  dfandc  896  pm4.63dc  898  pm4.54dc  914  pm4.79dc  915  orcanai  940  annimdc  950  pm4.55dc  951  orandc  952  pm4.82  963  pm3.11dc  970  pm3.12dc  971  dn1dc  973  3jcad  1209  3expia  1236  3an1rs  1250  3imp1  1251  3imp2  1253  syl3anl2  1327  3jaoian  1346  3jaodan  1347  mp3anl1  1372  mp3anl2  1373  mp3anl3  1374  ecased  1390  xor3dc  1436  pm5.15dc  1438  xor2dc  1439  xornbidc  1440  xordc  1441  nbbndc  1443  biassdc  1444  bilukdc  1445  dfbi3dc  1446  pm5.24dc  1447  xordidc  1448  alanimi  1512  19.29  1673  equs4  1777  equsexd  1782  spimth  1788  equs5a  1847  ax11v2  1873  ax11b  1879  equs5or  1883  sb5rf  1905  equvin  1916  nfsb4t  2074  eu5  2134  mopick  2165  euexex  2172  2euswapdc  2178  exists2  2184  eqrdav  2237  dvelimdc  2413  nebidc  2500  pm13.18  2501  nelne1  2510  nelne2  2511  rspa  2598  ralrimdvv  2634  r19.21bi  2638  r19.26  2677  ralbi  2683  rexbi  2684  r19.29  2688  vtoclgft  2873  rspcva  2927  rspc2va  2944  elabgt  2967  eqeu  2996  mob2  3006  mob  3008  euind  3013  reu6  3015  reuind  3031  sbctt  3118  rspsbca  3136  sbcnestgf  3199  rspcsbela  3207  ssel2  3243  sselda  3248  sstr  3256  nssne1  3306  nssne2  3307  reuss2  3513  reupick  3517  reupick2  3519  reximdva0m  3537  ssn0  3566  disjel  3579  ssdisj  3581  ifeqeqxdc  3687  absneu  3782  preqr1g  3889  prel12  3894  dfiun2g  4042  nbrne1  4147  nbrne2  4148  mpteq12f  4209  triun  4240  csbexga  4259  prcssprc  4272  iinexgm  4288  prexg  4347  copsex2t  4383  swopo  4449  poirr  4450  potr  4451  pofun  4455  issod  4462  ordelss  4522  trssord  4523  limelon  4542  trsuc  4565  eusvnfb  4598  rabxfrd  4613  regexmidlem1  4678  nordeq  4689  suc11g  4702  nnsuc  4761  brrelex12  4811  vtoclr  4821  optocl  4849  relop  4928  brcogw  4947  breldmg  4985  elreldm  5006  riinint  5041  xpexcnvm  5140  issref  5168  xpidtr  5176  trin2  5177  cnveqb  5241  funopg  5409  funssres  5418  fununi  5447  funimass2  5457  imain  5461  fnun  5487  fco  5550  opelf  5558  f0rn0  5585  f1oun  5657  fun11iun  5658  fv3  5716  ndmfvg  5724  fvelima  5751  fvopab3ig  5776  fvmptssdm  5787  fvmptf  5795  fvimacnv  5818  fmptco  5868  fcof  5888  funfvima2  5945  funfvima3  5946  f1veqaeq  5969  f1ocnvfvrneq  5982  fliftfun  5996  isotr  6016  isoini  6018  isopolem  6022  isosolem  6024  moriotass  6063  acexmidlem2  6076  suppssov1  6293  f1dmex  6339  elabreximd  6350  releldm2  6413  f1o2ndf1  6458  poxp  6462  fsuppeq  6481  suppssfvg  6497  tposf2  6533  iunon  6549  smoel2  6568  tfrlem9  6584  tfrexlem  6599  tfr1onlembxssdm  6608  tfr1onlemres  6614  tfrcllembxssdm  6621  tfrcllemres  6627  tfrcl  6629  tfri3  6632  frecabcl  6664  sucinc2  6713  nnacom  6751  nnmcom  6756  nnsucsssuc  6759  nnsucuniel  6762  nntri2or2  6765  nnaordi  6775  nnmordi  6783  nnaordex  6795  nnm00  6797  ectocld  6869  iinerm  6875  th3qlem2  6906  elpm2r  6934  mapsnd  6964  mapsncnv  6971  mptelixpg  7010  ixpsnf1o  7012  f1oen4g  7032  f1dom4g  7033  f1oen3g  7034  f1oeng  7037  en2d  7048  en3d  7049  dom2lem  7052  fundmen  7088  fundmeng  7089  unen  7099  modom  7102  rex2dom  7104  en2m  7107  xpdom2  7123  xpdom2g  7124  fopwdom  7130  nneneq  7152  phpm  7161  phpelm  7162  dif1enen  7178  fin0  7183  findcard  7186  diffifi  7192  ac6sfi  7196  onunsnss  7218  fiintim  7232  xpfi  7233  infidc  7242  fidcenum  7267  sbthlem1  7268  sbthlemi3  7270  sbthlemi10  7277  ffsuppbi  7294  elfir  7301  isotilem  7340  inflbti  7358  ordiso2  7369  eldju2ndl  7406  eldju2ndr  7407  updjudhf  7413  mkvprop  7492  carden2bex  7529  pm54.43  7530  exmidfodomrlemeldju  7545  exmidfodomrlemreseldju  7546  exmidfodomrlemim  7547  pw1m  7577  ltmpig  7700  enq0sym  7793  addnq0mo  7808  mulnq0mo  7809  prarloclem3step  7857  prarloclem3  7858  genpml  7878  genpmu  7879  genprndl  7882  genprndu  7883  genpdisj  7884  distrlem1prl  7943  distrlem1pru  7944  distrlem4prl  7945  distrlem4pru  7946  distrlem5prl  7947  distrlem5pru  7948  ltsopr  7957  ltaddpr  7958  addcanprleml  7975  addcanprlemu  7976  recexprlemm  7985  recexprlemlol  7987  recexprlemupu  7989  aptiprleml  8000  aptiprlemu  8001  caucvgprlemnkj  8027  caucvgprlemnbj  8028  addsrmo  8104  mulsrmo  8105  srpospr  8144  caucvgsr  8163  axprecex  8241  mpomulf  8310  mulgt0  8394  ltne  8404  cnegexlem1  8495  cnegexlem2  8496  negf1o  8703  addgt0  8770  addgegt0  8771  addgtge0  8772  addge0  8773  recexre  8900  mulge0  8941  recexap  8975  prodgt02  9177  prodge02  9179  ltmul12a  9184  mulgt1  9187  nndivtr  9329  addltmul  9525  elnnnn0b  9590  fcdmnn0supp  9598  fcdmnn0fsupp  9599  fcdmnn0suppg  9600  xnn0nnn0pnf  9626  elnnz  9637  zmulcl  9681  nn0n0n1ge2  9698  nn0lt2  9710  nn0le2is012  9711  uzind2  9741  nn0ind-raph  9746  eluzp1m1  9929  uz3m2nn  9956  supinfneg  9978  infsupneg  9979  infregelbex  9981  negm  9998  lbzbi  9999  qaddcl  10018  qmulcl  10020  qreccl  10025  elpq  10032  ledivge1le  10110  nn0ledivnn  10151  xrltne  10198  xrre  10205  xrre2  10206  xrre3  10207  ge0gtmnf  10208  xltnegi  10220  xnn0xadd0  10252  xnegdi  10253  xposdif  10267  xlesubadd  10268  iccsupr  10351  icoshft  10375  icoshftf1o  10376  fznlem  10428  fzen  10430  uzsubsubfz  10435  fzsuc2  10469  elfz1b  10480  elfz0ubfz0  10515  elfz0fzfz0  10516  fz0fzelfz0  10517  fz0fzdiffz0  10520  elfzmlbp  10522  difelfznle  10525  nn0p1elfzo  10577  fzofzim  10583  elincfzoext  10594  eluzgtdifelfzo  10598  elfzodifsumelfzo  10602  elfzonlteqm1  10611  elfzom1p1elfzo  10615  ssfzo12bi  10626  subfzo0  10644  zsupcllemex  10646  zssinfcl  10648  exbtwnzlemstep  10665  modqmuladdnn0  10788  modfzo0difsn  10815  addmodlteq  10818  frec2uzlt2d  10824  frecuzrdgtcl  10832  frecuzrdgfunlem  10839  seqf1og  10941  m1expcl2  10981  expge1  10996  leexp2r  11013  expubnd  11016  zesq  11079  expnlbnd  11085  nn0ltexp2  11130  nn0opthd  11143  faclbnd  11162  bcpasc  11187  hashprg  11232  hashf1  11270  seq3coll  11277  wrdnval  11318  wrdsymb0  11320  fstwrdne  11326  wrdred1hash  11331  swrdnd  11414  swrdwrdsymbg  11419  swrdsbslen  11421  swrdlsw  11424  swrdswrdlem  11459  swrdswrd  11460  pfxswrd  11461  cats1un  11476  wrd2ind  11478  swrdccatin1  11480  pfxccatin12lem4  11481  pfxccatin12lem2a  11482  pfxccatin12lem1  11483  swrdccatin2  11484  pfxccatin12lem2c  11485  pfxccatin12lem2  11486  pfxccatin12lem3  11487  pfxccatin12  11488  pfxccat3  11489  swrdccat  11490  pfxccat3a  11493  swrdccat3blem  11494  swrdccat3b  11495  swrdccatin2d  11499  reuccatpfxs1lem  11501  rexanuz  11737  rexuz3  11739  r19.29uz  11741  r19.2uz  11742  absnid  11822  leabs  11823  ltabs  11836  icodiamlt  11929  maxleast  11962  negfi  11977  climcn2  12058  climcau  12096  climcaucn  12100  sumdc  12107  fsum3cvg  12128  isumz  12139  fsumf1o  12140  fisumss  12142  isumss2  12143  fsumzcl2  12155  fsumsplit  12157  fsumsplitsnun  12169  sumsplitdc  12182  fsum2dlemstep  12184  telfsumo  12216  fsumparts  12220  fsumiun  12227  isumrpcl  12244  fproddccvg  12322  prod1dc  12336  prodssdc  12339  fprodssdc  12340  prodsnf  12342  fprodsplitdc  12346  fprod2dlemstep  12372  fprodmodd  12391  efexp  12432  efieq1re  12522  p1modz1  12544  dvds0lem  12551  dvds2ln  12574  dvdssub2  12585  dvdsadd2b  12590  dvdsabseq  12597  divconjdvds  12599  dvdsdivcl  12600  odd2np1  12623  oddge22np1  12631  opoe  12645  omoe  12646  opeo  12647  omeo  12648  m1expo  12650  nn0ehalf  12653  nn0o1gt2  12655  nno  12656  divalgb  12675  ndvdsadd  12681  bitsinv1lem  12711  gcd0id  12739  gcdneg  12742  gcdaddm  12744  bezoutlemstep  12757  dfgcd2  12774  gcddiv  12779  dvdsmulgcd  12785  bezoutr  12792  bezoutr1  12793  uzwodc  12797  nninfctlemfo  12800  algfx  12813  lcmgcdlem  12838  lcmgcdeq  12844  coprmdvds  12853  divgcdcoprmex  12863  cncongr1  12864  cncongr2  12865  isprm3  12879  dvdsnprmd  12886  prmgt1  12893  oddprmgt2  12895  isprm6  12908  cncongrprm  12918  phibndlem  12977  phimullem  12986  powm2modprm  13014  modprm0  13016  modprmn0modprm0  13018  prm23lt5  13025  pcneg  13087  pcprmpw2  13095  dvdsprmpweqnn  13098  dvdsprmpweqle  13099  pcaddlem  13101  fldivp1  13110  pcfac  13112  oddprmdvds  13116  prmunb  13124  ballotfilemfc0  13215  ballotfilemfcc  13216  ballotfilem4  13224  ballotfilemi1  13228  ballotfilemii  13229  ballotfilemic  13233  ballotfilem1c  13234  ballotfilemirc  13258  ballotfilem7  13262  ennnfone  13299  unct  13316  lidrididd  13685  sgrpass  13706  issgrpd  13710  issubmnd  13738  imasmnd2  13742  mnd1id  13746  insubm  13775  dfgrp2  13815  grpid  13827  grpasscan1  13851  dfgrp3mlem  13886  dfgrp3me  13888  imasgrp2  13896  mulgnn0gzsum  13914  mulgnn0p1  13919  mulgaddcom  13932  mulginvcom  13933  mulgass  13945  mulgpropdg  13950  subginv  13967  issubg2m  13975  issubg4m  13979  grpissubg  13980  resgrpisgrp  13981  subgintm  13984  kerf1ghm  14060  cmncom  14088  imasabl  14123  gsumvalfi  14135  rngdi  14222  rngdir  14223  rngpropd  14237  imasrng  14238  rng1zrlem  14241  imasring  14352  nzrunit  14478  issubrng2  14501  subrngintm  14503  issubrg2  14532  subrgintm  14534  lmodfopnelem1  14644  lmodfopnelem2  14645  lmodfopne  14646  islssm  14677  islidlm  14799  rnglidlmcl  14800  dflidl2rng  14801  rnglidlmmgm  14816  rnglidlmsgrp  14817  rnglidlrng  14818  gsumfsum  14906  dvdsrzring  14921  znidom  14975  issubassa3  14995  assamulgscmlem2  15025  uniopn  15085  istopon  15097  fiinbas  15133  tg2  15144  tgcl  15148  0nnei  15237  tgrest  15253  tgcn  15292  cnpnei  15303  cncnp2m  15315  lmtopcnp  15334  tx2cn  15354  txcn  15359  cnmpt21  15375  isxmet2d  15432  metrest  15590  metcnpi3  15601  tgioo  15638  fsumcncntop  15651  elcncf1di  15663  climcncf  15668  cncfco  15675  suplociccreex  15708  cnplimcim  15751  cnlimci  15757  reeff1olem  15855  efltlemlt  15858  pellexlem1  16074  zabsle1  16101  lgslem3  16104  lgsmod  16128  lgsdir2lem5  16134  lgsdir2  16135  lgsne0  16140  lgsdirnn0  16149  gausslemma2dlem0f  16156  gausslemma2dlem1a  16160  gausslemma2dlem3  16165  2lgslem1c  16192  2lgslem3a1  16199  2lgslem3b1  16200  2lgslem3c1  16201  2lgslem3d1  16202  2lgslem3  16203  2lgsoddprmlem2  16208  uhgrm  16302  incistruhgr  16314  upgrfnen  16322  umgrfnen  16332  umgrnloop  16340  upgredgpr  16373  usgrausgrben  16396  usgredgop  16397  usgruspgrben  16410  usgrislfuspgrdom  16414  umgrvad2edg  16435  ushgredgedg  16450  ushgredgedgloop  16452  uhgr0v0e  16458  subgreldmiedg  16493  subupgr  16497  uhgrspansubgrlem  16500  vtxdg0v  16518  wlkpropg  16548  wlkvg  16552  wlkl1loop  16582  upgriswlkdc  16584  upgrwlkedg  16585  upgrwlkvtxedg  16588  uspgr2wlkeq  16589  wlkres  16603  trlf1  16612  clwwlk1loop  16623  clwwlkccatlem  16624  isclwwlknx  16640  clwwlkn1loopb  16644  clwwlkext2edg  16646  umgr2cwwk2dif  16648  clwwlknonex2lem2  16662  clwwlknonex2  16663  eupthseg  16676  eupth2lem3lem4fi  16697  bj-charfun  16816  bj-charfunr  16819  bj-charfunbi  16820  bj-prexg  16920  peano5set  16949  bj-peano4  16964  bj-nn0suc  16973  bj-nn0sucALT  16987  bj-findis  16988  exmidsbthrlem  17041  trilpolemres  17065  trirec0  17067  nconstwlpolem  17089  neapmkv  17092  alsex  17113  ralsex  17114  als-no-surprise  17121