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

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem is used 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  3783  preqr1g  3891  prel12  3896  dfiun2g  4044  nbrne1  4149  nbrne2  4150  mpteq12f  4211  triun  4242  csbexga  4261  prcssprc  4274  iinexgm  4290  prexg  4349  copsex2t  4385  swopo  4451  poirr  4452  potr  4453  pofun  4457  issod  4464  ordelss  4524  trssord  4525  limelon  4544  trsuc  4567  eusvnfb  4600  rabxfrd  4615  regexmidlem1  4680  nordeq  4691  suc11g  4704  nnsuc  4763  brrelex12  4813  vtoclr  4823  optocl  4851  relop  4930  brcogw  4949  breldmg  4987  elreldm  5008  riinint  5043  xpexcnvm  5142  issref  5170  xpidtr  5178  trin2  5179  cnveqb  5243  funopg  5411  funssres  5420  fununi  5449  funimass2  5459  imain  5463  fnun  5489  fco  5552  opelf  5560  f0rn0  5587  f1oun  5659  fun11iun  5660  fv3  5718  ndmfvg  5726  fvelima  5754  fvopab3ig  5779  fvmptssdm  5790  fvmptf  5798  fvimacnv  5824  fmptco  5874  fcof  5894  funfvima2  5951  funfvima3  5952  f1veqaeq  5975  f1ocnvfvrneq  5988  fliftfun  6002  isotr  6022  isoini  6024  isopolem  6028  isosolem  6030  moriotass  6069  acexmidlem2  6082  suppssov1  6299  f1dmex  6345  elabreximd  6356  releldm2  6419  f1o2ndf1  6464  poxp  6468  fsuppeq  6487  suppssfvg  6503  tposf2  6539  iunon  6555  smoel2  6574  tfrlem9  6590  tfrexlem  6605  tfr1onlembxssdm  6614  tfr1onlemres  6620  tfrcllembxssdm  6627  tfrcllemres  6633  tfrcl  6635  tfri3  6638  frecabcl  6670  sucinc2  6719  nnacom  6757  nnmcom  6762  nnsucsssuc  6765  nnsucuniel  6768  nntri2or2  6771  nnaordi  6781  nnmordi  6789  nnaordex  6801  nnm00  6803  ectocld  6875  iinerm  6881  th3qlem2  6912  elpm2r  6940  mapsnd  6970  mapsncnv  6977  mptelixpg  7016  ixpsnf1o  7018  f1oen4g  7038  f1dom4g  7039  f1oen3g  7040  f1oeng  7043  en2d  7054  en3d  7055  dom2lem  7058  fundmen  7094  fundmeng  7095  unen  7105  modom  7108  rex2dom  7110  en2m  7113  xpdom2  7129  xpdom2g  7130  fopwdom  7136  nneneq  7158  phpm  7167  phpelm  7168  dif1enen  7184  fin0  7189  findcard  7192  diffifi  7198  ac6sfi  7202  onunsnss  7224  fiintim  7238  xpfi  7239  infidc  7248  fidcenum  7273  sbthlem1  7274  sbthlemi3  7276  sbthlemi10  7283  ffsuppbi  7300  elfir  7307  isotilem  7346  inflbti  7364  ordiso2  7375  eldju2ndl  7412  eldju2ndr  7413  updjudhf  7419  mkvprop  7498  carden2bex  7535  pm54.43  7536  exmidfodomrlemeldju  7551  exmidfodomrlemreseldju  7552  exmidfodomrlemim  7553  pw1m  7583  ltmpig  7706  enq0sym  7799  addnq0mo  7814  mulnq0mo  7815  prarloclem3step  7863  prarloclem3  7864  genpml  7884  genpmu  7885  genprndl  7888  genprndu  7889  genpdisj  7890  distrlem1prl  7949  distrlem1pru  7950  distrlem4prl  7951  distrlem4pru  7952  distrlem5prl  7953  distrlem5pru  7954  ltsopr  7963  ltaddpr  7964  addcanprleml  7981  addcanprlemu  7982  recexprlemm  7991  recexprlemlol  7993  recexprlemupu  7995  aptiprleml  8006  aptiprlemu  8007  caucvgprlemnkj  8033  caucvgprlemnbj  8034  addsrmo  8110  mulsrmo  8111  srpospr  8150  caucvgsr  8169  axprecex  8247  mpomulf  8316  mulgt0  8400  ltne  8410  cnegexlem1  8501  cnegexlem2  8502  negf1o  8709  addgt0  8776  addgegt0  8777  addgtge0  8778  addge0  8779  recexre  8907  mulge0  8948  recexap  8982  prodgt02  9184  prodge02  9186  ltmul12a  9191  mulgt1  9194  nndivtr  9347  addltmul  9544  elnnnn0b  9609  fcdmnn0supp  9617  fcdmnn0fsupp  9618  fcdmnn0suppg  9619  xnn0nnn0pnf  9645  elnnz  9656  zmulcl  9700  nn0n0n1ge2  9717  nn0lt2  9729  nn0le2is012  9730  uzind2  9760  nn0ind-raph  9765  eluzp1m1  9948  uz3m2nn  9975  supinfneg  9997  infsupneg  9998  infregelbex  10000  negm  10017  lbzbi  10018  qaddcl  10037  qmulcl  10039  qreccl  10044  elpq  10051  ledivge1le  10129  nn0ledivnn  10170  xrltne  10217  xrre  10224  xrre2  10225  xrre3  10226  ge0gtmnf  10227  xltnegi  10239  xnn0xadd0  10271  xnegdi  10272  xposdif  10286  xlesubadd  10287  iccsupr  10370  icoshft  10394  icoshftf1o  10395  fznlem  10447  fzen  10449  uzsubsubfz  10454  fzsuc2  10488  elfz1b  10499  elfz0ubfz0  10534  elfz0fzfz0  10535  fz0fzelfz0  10536  fz0fzdiffz0  10539  elfzmlbp  10541  difelfznle  10544  nn0p1elfzo  10596  fzofzim  10602  elincfzoext  10613  eluzgtdifelfzo  10617  elfzodifsumelfzo  10621  elfzonlteqm1  10630  elfzom1p1elfzo  10634  ssfzo12bi  10645  subfzo0  10663  zsupcllemex  10665  zssinfcl  10667  exbtwnzlemstep  10684  modqmuladdnn0  10807  modfzo0difsn  10834  addmodlteq  10837  frec2uzlt2d  10843  frecuzrdgtcl  10851  frecuzrdgfunlem  10858  seqf1og  10960  m1expcl2  11000  expge1  11015  leexp2r  11032  expubnd  11035  zesq  11098  expnlbnd  11104  nn0ltexp2  11149  nn0opthd  11162  faclbnd  11181  bcpasc  11206  hashprg  11251  hashf1  11289  seq3coll  11296  wrdnval  11337  wrdsymb0  11339  fstwrdne  11345  wrdred1hash  11350  swrdnd  11433  swrdwrdsymbg  11438  swrdsbslen  11440  swrdlsw  11443  swrdswrdlem  11478  swrdswrd  11479  pfxswrd  11480  cats1un  11495  wrd2ind  11497  swrdccatin1  11499  pfxccatin12lem4  11500  pfxccatin12lem2a  11501  pfxccatin12lem1  11502  swrdccatin2  11503  pfxccatin12lem2c  11504  pfxccatin12lem2  11505  pfxccatin12lem3  11506  pfxccatin12  11507  pfxccat3  11508  swrdccat  11509  pfxccat3a  11512  swrdccat3blem  11513  swrdccat3b  11514  swrdccatin2d  11518  reuccatpfxs1lem  11520  rexanuz  11756  rexuz3  11758  r19.29uz  11760  r19.2uz  11761  absnid  11841  leabs  11842  ltabs  11855  icodiamlt  11948  maxleast  11981  negfi  11996  climcn2  12077  climcau  12115  climcaucn  12119  sumdc  12126  fsum3cvg  12147  isumz  12158  fsumf1o  12159  fisumss  12161  isumss2  12162  fsumzcl2  12174  fsumsplit  12176  fsumsplitsnun  12188  sumsplitdc  12201  fsum2dlemstep  12203  telfsumo  12235  fsumparts  12239  fsumiun  12246  isumrpcl  12263  fproddccvg  12341  prod1dc  12355  prodssdc  12358  fprodssdc  12359  prodsnf  12361  fprodsplitdc  12365  fprod2dlemstep  12391  fprodmodd  12410  efexp  12451  efieq1re  12541  p1modz1  12563  dvds0lem  12570  dvds2ln  12593  dvdssub2  12604  dvdsadd2b  12609  dvdsabseq  12616  divconjdvds  12618  dvdsdivcl  12619  odd2np1  12642  oddge22np1  12650  opoe  12664  omoe  12665  opeo  12666  omeo  12667  m1expo  12669  nn0ehalf  12672  nn0o1gt2  12674  nno  12675  divalgb  12694  ndvdsadd  12700  bitsinv1lem  12730  gcd0id  12758  gcdneg  12761  gcdaddm  12763  bezoutlemstep  12776  dfgcd2  12793  gcddiv  12798  dvdsmulgcd  12804  bezoutr  12811  bezoutr1  12812  uzwodc  12816  nninfctlemfo  12819  algfx  12832  lcmgcdlem  12857  lcmgcdeq  12863  coprmdvds  12872  divgcdcoprmex  12882  cncongr1  12883  cncongr2  12884  isprm3  12898  dvdsnprmd  12905  prmgt1  12912  oddprmgt2  12914  isprm6  12927  cncongrprm  12937  phibndlem  12996  phimullem  13005  powm2modprm  13033  modprm0  13035  modprmn0modprm0  13037  prm23lt5  13044  pcneg  13106  pcprmpw2  13114  dvdsprmpweqnn  13117  dvdsprmpweqle  13118  pcaddlem  13120  fldivp1  13129  pcfac  13131  oddprmdvds  13135  prmunb  13143  ballotfilemfc0  13234  ballotfilemfcc  13235  ballotfilem4  13243  ballotfilemi1  13247  ballotfilemii  13248  ballotfilemic  13252  ballotfilem1c  13253  ballotfilemirc  13277  ballotfilem7  13281  ennnfone  13318  unct  13335  lidrididd  13704  sgrpass  13725  issgrpd  13729  issubmnd  13757  imasmnd2  13761  mnd1id  13765  insubm  13794  dfgrp2  13834  grpid  13846  grpasscan1  13870  dfgrp3mlem  13905  dfgrp3me  13907  imasgrp2  13915  mulgnn0gzsum  13933  mulgnn0p1  13938  mulgaddcom  13951  mulginvcom  13952  mulgass  13964  mulgpropdg  13969  subginv  13986  issubg2m  13994  issubg4m  13998  grpissubg  13999  resgrpisgrp  14000  subgintm  14003  kerf1ghm  14079  cmncom  14107  imasabl  14142  gsumvalfi  14154  rngdi  14241  rngdir  14242  rngpropd  14256  imasrng  14257  rng1zrlem  14260  imasring  14371  nzrunit  14497  issubrng2  14520  subrngintm  14522  issubrg2  14551  subrgintm  14553  lmodfopnelem1  14663  lmodfopnelem2  14664  lmodfopne  14665  islssm  14696  islidlm  14818  rnglidlmcl  14819  dflidl2rng  14820  rnglidlmmgm  14835  rnglidlmsgrp  14836  rnglidlrng  14837  gsumfsum  14925  dvdsrzring  14940  znidom  14994  issubassa3  15014  assamulgscmlem2  15044  uniopn  15104  istopon  15116  fiinbas  15152  tg2  15163  tgcl  15167  0nnei  15256  tgrest  15272  tgcn  15311  cnpnei  15322  cncnp2m  15334  lmtopcnp  15353  tx2cn  15373  txcn  15378  cnmpt21  15394  isxmet2d  15451  metrest  15609  metcnpi3  15620  tgioo  15657  fsumcncntop  15670  elcncf1di  15682  climcncf  15687  cncfco  15694  suplociccreex  15727  cnplimcim  15770  cnlimci  15776  reeff1olem  15874  efltlemlt  15877  efap1p  15882  pellexlem1  16097  zabsle1  16130  lgslem3  16133  lgsmod  16157  lgsdir2lem5  16163  lgsdir2  16164  lgsne0  16169  lgsdirnn0  16178  gausslemma2dlem0f  16185  gausslemma2dlem1a  16189  gausslemma2dlem3  16194  2lgslem1c  16221  2lgslem3a1  16228  2lgslem3b1  16229  2lgslem3c1  16230  2lgslem3d1  16231  2lgslem3  16232  2lgsoddprmlem2  16237  uhgrm  16331  incistruhgr  16343  upgrfnen  16351  umgrfnen  16361  umgrnloop  16369  upgredgpr  16402  usgrausgrben  16425  usgredgop  16426  usgruspgrben  16439  usgrislfuspgrdom  16443  umgrvad2edg  16464  ushgredgedg  16479  ushgredgedgloop  16481  uhgr0v0e  16487  subgreldmiedg  16522  subupgr  16526  uhgrspansubgrlem  16529  vtxdg0v  16547  wlkpropg  16577  wlkvg  16581  wlkl1loop  16611  upgriswlkdc  16613  upgrwlkedg  16614  upgrwlkvtxedg  16617  uspgr2wlkeq  16618  wlkres  16632  trlf1  16641  clwwlk1loop  16652  clwwlkccatlem  16653  isclwwlknx  16669  clwwlkn1loopb  16673  clwwlkext2edg  16675  umgr2cwwk2dif  16677  clwwlknonex2lem2  16691  clwwlknonex2  16692  eupthseg  16705  eupth2lem3lem4fi  16726  bj-charfun  16845  bj-charfunr  16848  bj-charfunbi  16849  bj-prexg  16949  peano5set  16978  bj-peano4  16993  bj-nn0suc  17002  bj-nn0sucALT  17016  bj-findis  17017  exmidsbthrlem  17079  trilpolemres  17103  trirec0  17105  nconstwlpolem  17127  neapmkv  17130  alsex  17151  ralsex  17152  als-no-surprise  17159