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  692  imnan  696  jaoian  802  jaodan  804  stdcndc  852  impidc  865  pm2.5gdc  873  con2bidc  882  pm5.18dc  890  dfandc  891  pm4.63dc  893  pm4.54dc  909  pm4.79dc  910  orcanai  935  annimdc  945  pm4.55dc  946  orandc  947  pm4.82  958  pm3.11dc  965  pm3.12dc  966  dn1dc  968  3jcad  1204  3expia  1231  3an1rs  1245  3imp1  1246  3imp2  1248  syl3anl2  1322  3jaoian  1341  3jaodan  1342  mp3anl1  1367  mp3anl2  1368  mp3anl3  1369  ecased  1385  xor3dc  1431  pm5.15dc  1433  xor2dc  1434  xornbidc  1435  xordc  1436  nbbndc  1438  biassdc  1439  bilukdc  1440  dfbi3dc  1441  pm5.24dc  1442  xordidc  1443  alanimi  1507  19.29  1668  equs4  1773  equsexd  1777  spimth  1783  equs5a  1842  ax11v2  1868  ax11b  1874  equs5or  1878  sb5rf  1900  equvin  1911  nfsb4t  2067  eu5  2127  mopick  2158  euexex  2165  2euswapdc  2171  exists2  2177  eqrdav  2230  dvelimdc  2395  nebidc  2482  pm13.18  2483  nelne1  2492  nelne2  2493  rspa  2580  ralrimdvv  2616  r19.21bi  2620  r19.26  2659  ralbi  2665  rexbi  2666  r19.29  2670  vtoclgft  2854  rspcva  2908  rspc2va  2924  elabgt  2947  eqeu  2976  mob2  2986  mob  2988  euind  2993  reu6  2995  reuind  3011  sbctt  3098  rspsbca  3116  sbcnestgf  3179  rspcsbela  3187  ssel2  3222  sselda  3227  sstr  3235  nssne1  3285  nssne2  3286  reuss2  3487  reupick  3491  reupick2  3493  reximdva0m  3510  ssn0  3537  disjel  3549  ssdisj  3551  absneu  3743  preqr1g  3849  prel12  3854  dfiun2g  4002  nbrne1  4107  nbrne2  4108  mpteq12f  4169  triun  4200  csbexga  4217  prcssprc  4230  iinexgm  4244  prexg  4301  copsex2t  4337  swopo  4403  poirr  4404  potr  4405  pofun  4409  issod  4416  ordelss  4476  trssord  4477  limelon  4496  trsuc  4519  eusvnfb  4551  rabxfrd  4566  regexmidlem1  4631  nordeq  4642  suc11g  4655  nnsuc  4714  brrelex12  4764  vtoclr  4774  optocl  4802  relop  4880  brcogw  4899  breldmg  4937  elreldm  4958  riinint  4993  issref  5119  xpidtr  5127  trin2  5128  cnveqb  5192  funopg  5360  funssres  5369  fununi  5398  funimass2  5408  imain  5412  fnun  5438  fco  5500  opelf  5507  f0rn0  5531  f1oun  5603  fun11iun  5604  fv3  5662  ndmfvg  5670  fvelima  5697  fvopab3ig  5720  fvmptssdm  5731  fvmptf  5739  fvimacnv  5762  fmptco  5813  fcof  5833  funfvima2  5887  funfvima3  5888  f1veqaeq  5910  f1ocnvfvrneq  5923  fliftfun  5937  isotr  5957  isoini  5959  isopolem  5963  isosolem  5965  moriotass  6002  acexmidlem2  6015  suppssfv  6231  suppssov1  6232  f1dmex  6278  releldm2  6348  f1o2ndf1  6393  poxp  6397  tposf2  6434  iunon  6450  smoel2  6469  tfrlem9  6485  tfrexlem  6500  tfr1onlembxssdm  6509  tfr1onlemres  6515  tfrcllembxssdm  6522  tfrcllemres  6528  tfrcl  6530  tfri3  6533  frecabcl  6565  sucinc2  6614  nnacom  6652  nnmcom  6657  nnsucsssuc  6660  nnsucuniel  6663  nntri2or2  6666  nnaordi  6676  nnmordi  6684  nnaordex  6696  nnm00  6698  ectocld  6770  iinerm  6776  th3qlem2  6807  elpm2r  6835  mapsncnv  6864  mptelixpg  6903  ixpsnf1o  6905  f1oen4g  6925  f1dom4g  6926  f1oen3g  6927  f1oeng  6930  en2d  6941  en3d  6942  dom2lem  6945  fundmen  6981  fundmeng  6982  unen  6991  modom  6994  rex2dom  6996  en2m  6999  xpdom2  7015  xpdom2g  7016  fopwdom  7022  nneneq  7043  phpm  7052  phpelm  7053  dif1enen  7069  fin0  7074  findcard  7077  diffifi  7083  ac6sfi  7087  onunsnss  7109  fiintim  7123  xpfi  7124  infidc  7133  fidcenum  7155  sbthlem1  7156  sbthlemi3  7158  sbthlemi10  7165  elfir  7172  isotilem  7205  inflbti  7223  ordiso2  7234  eldju2ndl  7271  eldju2ndr  7272  updjudhf  7278  mkvprop  7357  carden2bex  7394  pm54.43  7395  exmidfodomrlemeldju  7410  exmidfodomrlemreseldju  7411  exmidfodomrlemim  7412  pw1m  7442  ltmpig  7559  enq0sym  7652  addnq0mo  7667  mulnq0mo  7668  prarloclem3step  7716  prarloclem3  7717  genpml  7737  genpmu  7738  genprndl  7741  genprndu  7742  genpdisj  7743  distrlem1prl  7802  distrlem1pru  7803  distrlem4prl  7804  distrlem4pru  7805  distrlem5prl  7806  distrlem5pru  7807  ltsopr  7816  ltaddpr  7817  addcanprleml  7834  addcanprlemu  7835  recexprlemm  7844  recexprlemlol  7846  recexprlemupu  7848  aptiprleml  7859  aptiprlemu  7860  caucvgprlemnkj  7886  caucvgprlemnbj  7887  addsrmo  7963  mulsrmo  7964  srpospr  8003  caucvgsr  8022  axprecex  8100  mpomulf  8169  mulgt0  8254  ltne  8264  cnegexlem1  8354  cnegexlem2  8355  negf1o  8561  addgt0  8628  addgegt0  8629  addgtge0  8630  addge0  8631  recexre  8758  mulge0  8799  recexap  8833  prodgt02  9033  prodge02  9035  ltmul12a  9040  mulgt1  9043  nndivtr  9185  addltmul  9381  elnnnn0b  9446  xnn0nnn0pnf  9478  elnnz  9489  zmulcl  9533  nn0n0n1ge2  9550  nn0lt2  9561  nn0le2is012  9562  uzind2  9592  nn0ind-raph  9597  eluzp1m1  9780  uz3m2nn  9807  supinfneg  9829  infsupneg  9830  infregelbex  9832  negm  9849  lbzbi  9850  qaddcl  9869  qmulcl  9871  qreccl  9876  elpq  9883  ledivge1le  9961  nn0ledivnn  10002  xrltne  10048  xrre  10055  xrre2  10056  xrre3  10057  ge0gtmnf  10058  xltnegi  10070  xnn0xadd0  10102  xnegdi  10103  xposdif  10117  xlesubadd  10118  iccsupr  10201  icoshft  10225  icoshftf1o  10226  fznlem  10276  fzen  10278  uzsubsubfz  10282  fzsuc2  10314  elfz1b  10325  elfz0ubfz0  10360  elfz0fzfz0  10361  fz0fzelfz0  10362  fz0fzdiffz0  10365  elfzmlbp  10367  difelfznle  10370  nn0p1elfzo  10422  fzofzim  10428  elincfzoext  10439  eluzgtdifelfzo  10443  elfzodifsumelfzo  10447  elfzonlteqm1  10456  elfzom1p1elfzo  10460  ssfzo12bi  10471  subfzo0  10489  zsupcllemex  10491  zssinfcl  10493  exbtwnzlemstep  10508  modqmuladdnn0  10631  modfzo0difsn  10658  addmodlteq  10661  frec2uzlt2d  10667  frecuzrdgtcl  10675  frecuzrdgfunlem  10682  seqf1og  10784  m1expcl2  10824  expge1  10839  leexp2r  10856  expubnd  10859  zesq  10921  expnlbnd  10927  nn0ltexp2  10972  nn0opthd  10985  faclbnd  11004  bcpasc  11029  hashprg  11073  seq3coll  11107  wrdnval  11145  wrdsymb0  11147  fstwrdne  11153  wrdred1hash  11158  swrdnd  11241  swrdwrdsymbg  11246  swrdsbslen  11248  swrdlsw  11251  swrdswrdlem  11286  swrdswrd  11287  pfxswrd  11288  cats1un  11303  wrd2ind  11305  swrdccatin1  11307  pfxccatin12lem4  11308  pfxccatin12lem2a  11309  pfxccatin12lem1  11310  swrdccatin2  11311  pfxccatin12lem2c  11312  pfxccatin12lem2  11313  pfxccatin12lem3  11314  pfxccatin12  11315  pfxccat3  11316  swrdccat  11317  pfxccat3a  11320  swrdccat3blem  11321  swrdccat3b  11322  swrdccatin2d  11326  reuccatpfxs1lem  11328  rexanuz  11550  rexuz3  11552  r19.29uz  11554  r19.2uz  11555  absnid  11635  leabs  11636  ltabs  11649  icodiamlt  11742  maxleast  11775  negfi  11790  climcn2  11871  climcau  11909  climcaucn  11913  sumdc  11920  fsum3cvg  11941  isumz  11952  fsumf1o  11953  fisumss  11955  isumss2  11956  fsumzcl2  11968  fsumsplit  11970  fsumsplitsnun  11982  sumsplitdc  11995  fsum2dlemstep  11997  telfsumo  12029  fsumparts  12033  fsumiun  12040  isumrpcl  12057  fproddccvg  12135  prod1dc  12149  prodssdc  12152  fprodssdc  12153  prodsnf  12155  fprodsplitdc  12159  fprod2dlemstep  12185  fprodmodd  12204  efexp  12245  efieq1re  12335  p1modz1  12357  dvds0lem  12364  dvds2ln  12387  dvdssub2  12398  dvdsadd2b  12403  dvdsabseq  12410  divconjdvds  12412  dvdsdivcl  12413  odd2np1  12436  oddge22np1  12444  opoe  12458  omoe  12459  opeo  12460  omeo  12461  m1expo  12463  nn0ehalf  12466  nn0o1gt2  12468  nno  12469  divalgb  12488  ndvdsadd  12494  bitsinv1lem  12524  gcd0id  12552  gcdneg  12555  gcdaddm  12557  bezoutlemstep  12570  dfgcd2  12587  gcddiv  12592  dvdsmulgcd  12598  bezoutr  12605  bezoutr1  12606  uzwodc  12610  nninfctlemfo  12613  algfx  12626  lcmgcdlem  12651  lcmgcdeq  12657  coprmdvds  12666  divgcdcoprmex  12676  cncongr1  12677  cncongr2  12678  isprm3  12692  dvdsnprmd  12699  prmgt1  12706  oddprmgt2  12708  isprm6  12721  cncongrprm  12731  phibndlem  12790  phimullem  12799  powm2modprm  12827  modprm0  12829  modprmn0modprm0  12831  prm23lt5  12838  pcneg  12900  pcprmpw2  12908  dvdsprmpweqnn  12911  dvdsprmpweqle  12912  pcaddlem  12914  fldivp1  12923  pcfac  12925  oddprmdvds  12929  prmunb  12937  ennnfone  13048  unct  13065  lidrididd  13467  gsummgmpropd  13479  sgrpass  13493  issgrpd  13497  issubmnd  13527  imasmnd2  13537  mnd1id  13541  insubm  13570  dfgrp2  13612  grpid  13624  grpasscan1  13648  dfgrp3mlem  13683  dfgrp3me  13685  imasgrp2  13699  mulgnn0gsum  13717  mulgnn0p1  13722  mulgaddcom  13735  mulginvcom  13736  mulgass  13748  mulgpropdg  13753  subginv  13770  issubg2m  13778  issubg4m  13782  grpissubg  13783  resgrpisgrp  13784  subgintm  13787  kerf1ghm  13863  cmncom  13891  imasabl  13925  rngdi  13956  rngdir  13957  rngpropd  13971  imasrng  13972  imasring  14080  nzrunit  14205  issubrng2  14227  subrngintm  14229  issubrg2  14258  subrgintm  14260  lmodfopnelem1  14341  lmodfopnelem2  14342  lmodfopne  14343  islssm  14374  islidlm  14496  rnglidlmcl  14497  dflidl2rng  14498  rnglidlmmgm  14513  rnglidlmsgrp  14514  rnglidlrng  14515  dvdsrzring  14620  znidom  14674  uniopn  14728  istopon  14740  fiinbas  14776  tg2  14787  tgcl  14791  0nnei  14880  tgrest  14896  tgcn  14935  cnpnei  14946  cncnp2m  14958  lmtopcnp  14977  tx2cn  14997  txcn  15002  cnmpt21  15018  isxmet2d  15075  metrest  15233  metcnpi3  15244  tgioo  15281  fsumcncntop  15294  elcncf1di  15306  climcncf  15311  cncfco  15318  suplociccreex  15351  cnplimcim  15394  cnlimci  15400  reeff1olem  15498  efltlemlt  15501  zabsle1  15731  lgslem3  15734  lgsmod  15758  lgsdir2lem5  15764  lgsdir2  15765  lgsne0  15770  lgsdirnn0  15779  gausslemma2dlem0f  15786  gausslemma2dlem1a  15790  gausslemma2dlem3  15795  2lgslem1c  15822  2lgslem3a1  15829  2lgslem3b1  15830  2lgslem3c1  15831  2lgslem3d1  15832  2lgslem3  15833  2lgsoddprmlem2  15838  uhgrm  15932  incistruhgr  15944  upgrfnen  15952  umgrfnen  15962  umgrnloop  15970  upgredgpr  16003  usgrausgrben  16026  usgredgop  16027  usgruspgrben  16040  usgrislfuspgrdom  16044  umgrvad2edg  16065  ushgredgedg  16080  ushgredgedgloop  16082  uhgr0v0e  16088  subgreldmiedg  16123  subupgr  16127  uhgrspansubgrlem  16130  vtxdg0v  16148  wlkpropg  16178  wlkvg  16182  wlkl1loop  16212  upgriswlkdc  16214  upgrwlkedg  16215  upgrwlkvtxedg  16218  uspgr2wlkeq  16219  wlkres  16233  trlf1  16242  clwwlk1loop  16253  clwwlkccatlem  16254  isclwwlknx  16270  clwwlkn1loopb  16274  clwwlkext2edg  16276  umgr2cwwk2dif  16278  clwwlknonex2lem2  16292  clwwlknonex2  16293  eupthseg  16306  eupth2lem3lem4fi  16327  bj-charfun  16423  bj-charfunr  16426  bj-charfunbi  16427  bj-prexg  16527  peano5set  16556  bj-peano4  16571  bj-nn0suc  16580  bj-nn0sucALT  16594  bj-findis  16595  exmidsbthrlem  16647  trilpolemres  16667  trirec0  16669  nconstwlpolem  16690  neapmkv  16693  gfsumval  16701