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  4150  nbrne2  4151  mpteq12f  4212  triun  4244  csbexga  4263  prcssprc  4276  iinexgm  4292  prexg  4351  copsex2t  4387  swopo  4453  poirr  4454  potr  4455  pofun  4459  issod  4466  ordelss  4526  trssord  4527  limelon  4546  trsuc  4569  eusvnfb  4602  rabxfrd  4617  regexmidlem1  4682  nordeq  4693  suc11g  4706  nnsuc  4765  brrelex12  4815  vtoclr  4825  optocl  4853  relop  4932  brcogw  4951  breldmg  4989  elreldm  5010  riinint  5045  xpexcnvm  5145  issref  5173  xpidtr  5181  trin2  5182  cnveqb  5246  funopg  5414  funssres  5423  fununi  5452  funimass2  5462  imain  5466  fnun  5492  fco  5555  opelf  5563  f0rn0  5590  f1oun  5662  fun11iun  5663  fv3  5721  ndmfvg  5729  fvelima  5757  fvopab3ig  5782  fvmptssdm  5793  fvmptf  5801  fvimacnv  5827  fmptco  5877  fcof  5897  funfvima2  5954  funfvima3  5955  f1veqaeq  5978  f1ocnvfvrneq  5991  fliftfun  6005  isotr  6025  isoini  6027  isopolem  6031  isosolem  6033  moriotass  6072  acexmidlem2  6085  suppssov1  6302  f1dmex  6349  elabreximd  6360  releldm2  6423  f1o2ndf1  6468  poxp  6472  fsuppeq  6491  suppssfvg  6507  tposf2  6543  iunon  6559  smoel2  6578  tfrlem9  6594  tfrexlem  6609  tfr1onlembxssdm  6618  tfr1onlemres  6624  tfrcllembxssdm  6631  tfrcllemres  6637  tfrcl  6639  tfri3  6642  frecabcl  6674  sucinc2  6723  nnacom  6761  nnmcom  6766  nnsucsssuc  6769  nnsucuniel  6772  nntri2or2  6775  nnaordi  6785  nnmordi  6793  nnaordex  6805  nnm00  6807  ectocld  6879  iinerm  6885  th3qlem2  6916  elpm2r  6944  mapsnd  6975  mapsncnv  6982  mptelixpg  7021  ixpsnf1o  7023  f1oen4g  7043  f1dom4g  7044  f1oen3g  7045  f1oeng  7048  en2d  7059  en3d  7060  dom2lem  7063  fundmen  7099  fundmeng  7100  unen  7110  modom  7113  rex2dom  7115  en2m  7118  xpdom2  7134  xpdom2g  7135  fopwdom  7141  nneneq  7163  phpm  7172  phpelm  7173  dif1enen  7189  fin0  7194  findcard  7197  diffifi  7203  ac6sfi  7207  onunsnss  7229  fiintim  7243  xpfi  7244  infidc  7253  fidcenum  7279  sbthlem1  7280  sbthlemi3  7282  sbthlemi10  7289  ffsuppbi  7306  elfir  7313  isotilem  7353  inflbti  7371  ordiso2  7382  eldju2ndl  7419  eldju2ndr  7420  updjudhf  7426  mkvprop  7505  carden2bex  7542  pm54.43  7543  exmidfodomrlemeldju  7558  exmidfodomrlemreseldju  7559  exmidfodomrlemim  7560  pw1m  7590  ltmpig  7713  enq0sym  7806  addnq0mo  7821  mulnq0mo  7822  prarloclem3step  7870  prarloclem3  7871  genpml  7891  genpmu  7892  genprndl  7895  genprndu  7896  genpdisj  7897  distrlem1prl  7956  distrlem1pru  7957  distrlem4prl  7958  distrlem4pru  7959  distrlem5prl  7960  distrlem5pru  7961  ltsopr  7970  ltaddpr  7971  addcanprleml  7988  addcanprlemu  7989  recexprlemm  7998  recexprlemlol  8000  recexprlemupu  8002  aptiprleml  8013  aptiprlemu  8014  caucvgprlemnkj  8040  caucvgprlemnbj  8041  addsrmo  8117  mulsrmo  8118  srpospr  8157  caucvgsr  8176  axprecex  8254  mpomulf  8323  mulgt0  8407  ltne  8417  cnegexlem1  8509  cnegexlem2  8510  negf1o  8717  addgt0  8784  addgegt0  8785  addgtge0  8786  addge0  8787  recexre  8915  mulge0  8956  recexap  8990  prodgt02  9192  prodge02  9194  ltmul12a  9199  mulgt1  9202  nndivtr  9356  addltmul  9554  elnnnn0b  9619  fcdmnn0supp  9627  fcdmnn0fsupp  9628  fcdmnn0suppg  9629  xnn0nnn0pnf  9655  elnnz  9666  zmulcl  9710  nn0n0n1ge2  9727  nn0lt2  9739  nn0le2is012  9740  uzind2  9770  nn0ind-raph  9775  eluzp1m1  9963  uz3m2nn  9990  supinfneg  10012  infsupneg  10013  infregelbex  10015  negm  10032  lbzbi  10033  qaddcl  10052  qmulcl  10054  qreccl  10059  elpq  10067  ledivge1le  10145  nn0ledivnn  10186  xrltne  10233  xrre  10240  xrre2  10241  xrre3  10242  ge0gtmnf  10243  xltnegi  10255  xnn0xadd0  10287  xnegdi  10288  xposdif  10302  xlesubadd  10303  iccsupr  10386  icoshft  10410  icoshftf1o  10411  fznlem  10463  fzen  10465  uzsubsubfz  10470  fzsuc2  10504  elfz1b  10515  elfz0ubfz0  10550  elfz0fzfz0  10551  fz0fzelfz0  10552  fz0fzdiffz0  10555  elfzmlbp  10557  difelfznle  10560  nn0p1elfzo  10612  fzofzim  10618  elincfzoext  10629  eluzgtdifelfzo  10633  elfzodifsumelfzo  10637  elfzonlteqm1  10646  elfzom1p1elfzo  10650  ssfzo12bi  10661  subfzo0  10679  zsupcllemex  10681  zssinfcl  10683  exbtwnzlemstep  10700  modqmuladdnn0  10827  modfzo0difsn  10854  addmodlteq  10857  frec2uzlt2d  10863  frecuzrdgtcl  10871  frecuzrdgfunlem  10878  seqf1og  10980  m1expcl2  11020  expge1  11035  leexp2r  11052  expubnd  11055  zesq  11118  expnlbnd  11124  nn0ltexp2  11170  nn0opthd  11183  faclbnd  11202  bcpasc  11227  hashprg  11272  hashf1  11310  seq3coll  11317  wrdnval  11358  wrdsymb0  11360  fstwrdne  11366  wrdred1hash  11371  swrdnd  11454  swrdwrdsymbg  11459  swrdsbslen  11461  swrdlsw  11464  swrdswrdlem  11499  swrdswrd  11500  pfxswrd  11501  cats1un  11516  wrd2ind  11518  swrdccatin1  11520  pfxccatin12lem4  11521  pfxccatin12lem2a  11522  pfxccatin12lem1  11523  swrdccatin2  11524  pfxccatin12lem2c  11525  pfxccatin12lem2  11526  pfxccatin12lem3  11527  pfxccatin12  11528  pfxccat3  11529  swrdccat  11530  pfxccat3a  11533  swrdccat3blem  11534  swrdccat3b  11535  swrdccatin2d  11539  reuccatpfxs1lem  11541  rexanuz  11777  rexuz3  11779  r19.29uz  11781  r19.2uz  11782  absnid  11862  leabs  11863  ltabs  11877  icodiamlt  11970  maxleast  12003  negfi  12018  climcn2  12101  climcau  12139  climcaucn  12143  sumdc  12150  fsum3cvg  12171  isumz  12182  fsumf1o  12183  fisumss  12185  isumss2  12186  fsumzcl2  12198  fsumsplit  12200  fsumsplitsnun  12212  sumsplitdc  12225  fsum2dlemstep  12227  telfsumo  12259  fsumparts  12263  fsumiun  12270  isumrpcl  12287  fproddccvg  12365  prod1dc  12379  prodssdc  12382  fprodssdc  12383  prodsnf  12385  fprodsplitdc  12389  fprod2dlemstep  12415  fprodmodd  12434  efexp  12475  efieq1re  12565  p1modz1  12587  dvds0lem  12594  dvds2ln  12617  dvdssub2  12628  dvdsadd2b  12633  dvdsabseq  12640  divconjdvds  12642  dvdsdivcl  12643  odd2np1  12666  oddge22np1  12674  opoe  12688  omoe  12689  opeo  12690  omeo  12691  m1expo  12693  nn0ehalf  12696  nn0o1gt2  12698  nno  12699  divalgb  12718  ndvdsadd  12724  bitsinv1lem  12754  gcd0id  12782  gcdneg  12785  gcdaddm  12787  bezoutlemstep  12800  dfgcd2  12817  gcddiv  12822  dvdsmulgcd  12828  bezoutr  12835  bezoutr1  12836  uzwodc  12840  nninfctlemfo  12843  algfx  12856  lcmgcdlem  12881  lcmgcdeq  12887  coprmdvds  12896  divgcdcoprmex  12906  cncongr1  12907  cncongr2  12908  isprm3  12922  dvdsnprmd  12929  prmgt1  12937  oddprmgt2  12939  isprm6  12952  cncongrprm  12962  phibndlem  13024  phimullem  13033  powm2modprm  13061  modprm0  13063  modprmn0modprm0  13065  prm23lt5  13072  pcneg  13134  pcprmpw2  13142  dvdsprmpweqnn  13145  dvdsprmpweqle  13146  pcaddlem  13148  fldivp1  13157  pcfac  13159  oddprmdvds  13163  prmunb  13171  ballotfilemfc0  13291  ballotfilemfcc  13292  ballotfilem4  13300  ballotfilemi1  13304  ballotfilemii  13305  ballotfilemic  13309  ballotfilem1c  13310  ballotfilemirc  13334  ballotfilem7  13338  ennnfone  13375  unct  13392  lidrididd  13762  sgrpass  13783  issgrpd  13787  issubmnd  13815  imasmnd2  13819  mnd1id  13823  insubm  13852  dfgrp2  13892  grpid  13904  grpasscan1  13928  dfgrp3mlem  13963  dfgrp3me  13965  imasgrp2  13973  mulgnn0gzsum  13991  mulgnn0p1  13996  mulgaddcom  14009  mulginvcom  14010  mulgass  14022  mulgpropdg  14027  subginv  14044  issubg2m  14052  issubg4m  14056  grpissubg  14057  resgrpisgrp  14058  subgintm  14061  kerf1ghm  14137  cmncom  14196  imasabl  14231  gsumvalfi  14243  rngdi  14347  rngdir  14348  rngpropd  14362  imasrng  14363  rng1zrlem  14366  imasring  14479  nzrunit  14605  issubrng2  14628  subrngintm  14630  issubrg2  14659  subrgintm  14661  lmodfopnelem1  14771  lmodfopnelem2  14772  lmodfopne  14773  islssm  14804  islidlm  14926  rnglidlmcl  14927  dflidl2rng  14928  rnglidlmmgm  14943  rnglidlmsgrp  14944  rnglidlrng  14945  gsumfsum  15033  dvdsrzring  15048  znidom  15102  issubassa3  15122  assamulgscmlem2  15152  uniopn  15239  istopon  15251  fiinbas  15287  tg2  15298  tgcl  15302  0nnei  15391  tgrest  15407  tgcn  15446  cnpnei  15457  cncnp2m  15469  lmtopcnp  15488  tx2cn  15508  txcn  15513  cnmpt21  15529  isxmet2d  15586  metrest  15744  metcnpi3  15755  tgioo  15792  fsumcncntop  15805  elcncf1di  15817  climcncf  15822  cncfco  15829  suplociccreex  15862  cnplimcim  15905  cnlimci  15911  reeff1olem  16009  efltlemlt  16012  efap1p  16017  sineq0re  16088  pellexlem1  16241  chtqub  16308  bpos1  16322  bposlem6  16328  zabsle1  16335  lgslem3  16338  lgsmod  16362  lgsdir2lem5  16368  lgsdir2  16369  lgsne0  16374  lgsdirnn0  16383  gausslemma2dlem0f  16390  gausslemma2dlem1a  16394  gausslemma2dlem3  16399  2lgslem1c  16426  2lgslem3a1  16433  2lgslem3b1  16434  2lgslem3c1  16435  2lgslem3d1  16436  2lgslem3  16437  2lgsoddprmlem2  16442  uhgrm  16536  incistruhgr  16548  upgrfnen  16556  umgrfnen  16566  umgrnloop  16574  upgredgpr  16607  usgrausgrben  16630  usgredgop  16631  usgruspgrben  16644  usgrislfuspgrdom  16648  umgrvad2edg  16669  ushgredgedg  16684  ushgredgedgloop  16686  uhgr0v0e  16692  subgreldmiedg  16727  subupgr  16731  uhgrspansubgrlem  16734  vtxdg0v  16752  wlkpropg  16782  wlkvg  16786  wlkl1loop  16816  upgriswlkdc  16818  upgrwlkedg  16819  upgrwlkvtxedg  16822  uspgr2wlkeq  16823  wlkres  16837  trlf1  16846  clwwlk1loop  16857  clwwlkccatlem  16858  isclwwlknx  16874  clwwlkn1loopb  16878  clwwlkext2edg  16880  umgr2cwwk2dif  16882  clwwlknonex2lem2  16896  clwwlknonex2  16897  eupthseg  16910  eupth2lem3lem4fi  16931  bj-charfun  17050  bj-charfunr  17053  bj-charfunbi  17054  bj-prexg  17154  peano5set  17183  bj-peano4  17198  bj-nn0suc  17207  bj-nn0sucALT  17221  bj-findis  17222  exmidsbthrlem  17285  trilpolemres  17310  trirec0  17312  nconstwlpolem  17334  neapmkv  17337  alsex  17358  ralsex  17359  als-no-surprise  17366