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  2938  elabgt  2961  eqeu  2990  mob2  3000  mob  3002  euind  3007  reu6  3009  reuind  3025  sbctt  3112  rspsbca  3130  sbcnestgf  3193  rspcsbela  3201  ssel2  3237  sselda  3242  sstr  3250  nssne1  3300  nssne2  3301  reuss2  3505  reupick  3509  reupick2  3511  reximdva0m  3528  ssn0  3555  disjel  3567  ssdisj  3569  ifeqeqxdc  3673  absneu  3768  preqr1g  3875  prel12  3880  dfiun2g  4028  nbrne1  4133  nbrne2  4134  mpteq12f  4195  triun  4226  csbexga  4243  prcssprc  4256  iinexgm  4271  prexg  4330  copsex2t  4366  swopo  4432  poirr  4433  potr  4434  pofun  4438  issod  4445  ordelss  4505  trssord  4506  limelon  4525  trsuc  4548  eusvnfb  4580  rabxfrd  4595  regexmidlem1  4660  nordeq  4671  suc11g  4684  nnsuc  4743  brrelex12  4793  vtoclr  4803  optocl  4831  relop  4910  brcogw  4929  breldmg  4967  elreldm  4988  riinint  5023  xpexcnvm  5122  issref  5150  xpidtr  5158  trin2  5159  cnveqb  5223  funopg  5391  funssres  5400  fununi  5429  funimass2  5439  imain  5443  fnun  5469  fco  5532  opelf  5540  f0rn0  5567  f1oun  5639  fun11iun  5640  fv3  5698  ndmfvg  5706  fvelima  5733  fvopab3ig  5756  fvmptssdm  5767  fvmptf  5775  fvimacnv  5798  fmptco  5848  fcof  5868  funfvima2  5924  funfvima3  5925  f1veqaeq  5948  f1ocnvfvrneq  5961  fliftfun  5975  isotr  5995  isoini  5997  isopolem  6001  isosolem  6003  moriotass  6042  acexmidlem2  6055  suppssov1  6272  f1dmex  6318  elabreximd  6329  releldm2  6392  f1o2ndf1  6437  poxp  6441  fsuppeq  6460  suppssfvg  6476  tposf2  6512  iunon  6528  smoel2  6547  tfrlem9  6563  tfrexlem  6578  tfr1onlembxssdm  6587  tfr1onlemres  6593  tfrcllembxssdm  6600  tfrcllemres  6606  tfrcl  6608  tfri3  6611  frecabcl  6643  sucinc2  6692  nnacom  6730  nnmcom  6735  nnsucsssuc  6738  nnsucuniel  6741  nntri2or2  6744  nnaordi  6754  nnmordi  6762  nnaordex  6774  nnm00  6776  ectocld  6848  iinerm  6854  th3qlem2  6885  elpm2r  6913  mapsnd  6936  mapsncnv  6943  mptelixpg  6982  ixpsnf1o  6984  f1oen4g  7004  f1dom4g  7005  f1oen3g  7006  f1oeng  7009  en2d  7020  en3d  7021  dom2lem  7024  fundmen  7060  fundmeng  7061  unen  7071  modom  7074  rex2dom  7076  en2m  7079  xpdom2  7095  xpdom2g  7096  fopwdom  7102  nneneq  7124  phpm  7133  phpelm  7134  dif1enen  7150  fin0  7155  findcard  7158  diffifi  7164  ac6sfi  7168  onunsnss  7190  fiintim  7204  xpfi  7205  infidc  7214  fidcenum  7239  sbthlem1  7240  sbthlemi3  7242  sbthlemi10  7249  ffsuppbi  7266  elfir  7273  isotilem  7310  inflbti  7328  ordiso2  7339  eldju2ndl  7376  eldju2ndr  7377  updjudhf  7383  mkvprop  7462  carden2bex  7499  pm54.43  7500  exmidfodomrlemeldju  7515  exmidfodomrlemreseldju  7516  exmidfodomrlemim  7517  pw1m  7547  ltmpig  7670  enq0sym  7763  addnq0mo  7778  mulnq0mo  7779  prarloclem3step  7827  prarloclem3  7828  genpml  7848  genpmu  7849  genprndl  7852  genprndu  7853  genpdisj  7854  distrlem1prl  7913  distrlem1pru  7914  distrlem4prl  7915  distrlem4pru  7916  distrlem5prl  7917  distrlem5pru  7918  ltsopr  7927  ltaddpr  7928  addcanprleml  7945  addcanprlemu  7946  recexprlemm  7955  recexprlemlol  7957  recexprlemupu  7959  aptiprleml  7970  aptiprlemu  7971  caucvgprlemnkj  7997  caucvgprlemnbj  7998  addsrmo  8074  mulsrmo  8075  srpospr  8114  caucvgsr  8133  axprecex  8211  mpomulf  8280  mulgt0  8364  ltne  8374  cnegexlem1  8465  cnegexlem2  8466  negf1o  8673  addgt0  8740  addgegt0  8741  addgtge0  8742  addge0  8743  recexre  8870  mulge0  8911  recexap  8945  prodgt02  9147  prodge02  9149  ltmul12a  9154  mulgt1  9157  nndivtr  9299  addltmul  9495  elnnnn0b  9560  fcdmnn0supp  9568  fcdmnn0fsupp  9569  fcdmnn0suppg  9570  xnn0nnn0pnf  9596  elnnz  9607  zmulcl  9651  nn0n0n1ge2  9668  nn0lt2  9680  nn0le2is012  9681  uzind2  9711  nn0ind-raph  9716  eluzp1m1  9899  uz3m2nn  9926  supinfneg  9948  infsupneg  9949  infregelbex  9951  negm  9968  lbzbi  9969  qaddcl  9988  qmulcl  9990  qreccl  9995  elpq  10002  ledivge1le  10080  nn0ledivnn  10121  xrltne  10168  xrre  10175  xrre2  10176  xrre3  10177  ge0gtmnf  10178  xltnegi  10190  xnn0xadd0  10222  xnegdi  10223  xposdif  10237  xlesubadd  10238  iccsupr  10321  icoshft  10345  icoshftf1o  10346  fznlem  10398  fzen  10400  uzsubsubfz  10404  fzsuc2  10438  elfz1b  10449  elfz0ubfz0  10484  elfz0fzfz0  10485  fz0fzelfz0  10486  fz0fzdiffz0  10489  elfzmlbp  10491  difelfznle  10494  nn0p1elfzo  10546  fzofzim  10552  elincfzoext  10563  eluzgtdifelfzo  10567  elfzodifsumelfzo  10571  elfzonlteqm1  10580  elfzom1p1elfzo  10584  ssfzo12bi  10595  subfzo0  10613  zsupcllemex  10615  zssinfcl  10617  exbtwnzlemstep  10634  modqmuladdnn0  10757  modfzo0difsn  10784  addmodlteq  10787  frec2uzlt2d  10793  frecuzrdgtcl  10801  frecuzrdgfunlem  10808  seqf1og  10910  m1expcl2  10950  expge1  10965  leexp2r  10982  expubnd  10985  zesq  11048  expnlbnd  11054  nn0ltexp2  11099  nn0opthd  11112  faclbnd  11131  bcpasc  11156  hashprg  11201  seq3coll  11242  wrdnval  11283  wrdsymb0  11285  fstwrdne  11291  wrdred1hash  11296  swrdnd  11379  swrdwrdsymbg  11384  swrdsbslen  11386  swrdlsw  11389  swrdswrdlem  11424  swrdswrd  11425  pfxswrd  11426  cats1un  11441  wrd2ind  11443  swrdccatin1  11445  pfxccatin12lem4  11446  pfxccatin12lem2a  11447  pfxccatin12lem1  11448  swrdccatin2  11449  pfxccatin12lem2c  11450  pfxccatin12lem2  11451  pfxccatin12lem3  11452  pfxccatin12  11453  pfxccat3  11454  swrdccat  11455  pfxccat3a  11458  swrdccat3blem  11459  swrdccat3b  11460  swrdccatin2d  11464  reuccatpfxs1lem  11466  rexanuz  11701  rexuz3  11703  r19.29uz  11705  r19.2uz  11706  absnid  11786  leabs  11787  ltabs  11800  icodiamlt  11893  maxleast  11926  negfi  11941  climcn2  12022  climcau  12060  climcaucn  12064  sumdc  12071  fsum3cvg  12092  isumz  12103  fsumf1o  12104  fisumss  12106  isumss2  12107  fsumzcl2  12119  fsumsplit  12121  fsumsplitsnun  12133  sumsplitdc  12146  fsum2dlemstep  12148  telfsumo  12180  fsumparts  12184  fsumiun  12191  isumrpcl  12208  fproddccvg  12286  prod1dc  12300  prodssdc  12303  fprodssdc  12304  prodsnf  12306  fprodsplitdc  12310  fprod2dlemstep  12336  fprodmodd  12355  efexp  12396  efieq1re  12486  p1modz1  12508  dvds0lem  12515  dvds2ln  12538  dvdssub2  12549  dvdsadd2b  12554  dvdsabseq  12561  divconjdvds  12563  dvdsdivcl  12564  odd2np1  12587  oddge22np1  12595  opoe  12609  omoe  12610  opeo  12611  omeo  12612  m1expo  12614  nn0ehalf  12617  nn0o1gt2  12619  nno  12620  divalgb  12639  ndvdsadd  12645  bitsinv1lem  12675  gcd0id  12703  gcdneg  12706  gcdaddm  12708  bezoutlemstep  12721  dfgcd2  12738  gcddiv  12743  dvdsmulgcd  12749  bezoutr  12756  bezoutr1  12757  uzwodc  12761  nninfctlemfo  12764  algfx  12777  lcmgcdlem  12802  lcmgcdeq  12808  coprmdvds  12817  divgcdcoprmex  12827  cncongr1  12828  cncongr2  12829  isprm3  12843  dvdsnprmd  12850  prmgt1  12857  oddprmgt2  12859  isprm6  12872  cncongrprm  12882  phibndlem  12941  phimullem  12950  powm2modprm  12978  modprm0  12980  modprmn0modprm0  12982  prm23lt5  12989  pcneg  13051  pcprmpw2  13059  dvdsprmpweqnn  13062  dvdsprmpweqle  13063  pcaddlem  13065  fldivp1  13074  pcfac  13076  oddprmdvds  13080  prmunb  13088  ballotfilemfc0  13179  ballotfilemfcc  13180  ballotfilem4  13188  ballotfilemi1  13192  ballotfilemii  13193  ballotfilemic  13197  ballotfilem1c  13198  ballotfilemirc  13222  ballotfilem7  13226  ennnfone  13263  unct  13280  lidrididd  13648  gsummgmpropd  13660  sgrpass  13674  issgrpd  13678  issubmnd  13706  imasmnd2  13710  mnd1id  13714  insubm  13743  dfgrp2  13785  grpid  13797  grpasscan1  13821  dfgrp3mlem  13856  dfgrp3me  13858  imasgrp2  13866  mulgnn0gsum  13884  mulgnn0p1  13889  mulgaddcom  13902  mulginvcom  13903  mulgass  13915  mulgpropdg  13920  subginv  13937  issubg2m  13945  issubg4m  13949  grpissubg  13950  resgrpisgrp  13951  subgintm  13954  kerf1ghm  14030  cmncom  14058  imasabl  14092  gfsumval  14105  rngdi  14182  rngdir  14183  rngpropd  14197  imasrng  14198  rng1zrlem  14201  imasring  14310  nzrunit  14436  issubrng2  14459  subrngintm  14461  issubrg2  14490  subrgintm  14492  lmodfopnelem1  14601  lmodfopnelem2  14602  lmodfopne  14603  islssm  14634  islidlm  14756  rnglidlmcl  14757  dflidl2rng  14758  rnglidlmmgm  14773  rnglidlmsgrp  14774  rnglidlrng  14775  dvdsrzring  14880  znidom  14934  uniopn  14995  istopon  15007  fiinbas  15043  tg2  15054  tgcl  15058  0nnei  15147  tgrest  15163  tgcn  15202  cnpnei  15213  cncnp2m  15225  lmtopcnp  15244  tx2cn  15264  txcn  15269  cnmpt21  15285  isxmet2d  15342  metrest  15500  metcnpi3  15511  tgioo  15548  fsumcncntop  15561  elcncf1di  15573  climcncf  15578  cncfco  15585  suplociccreex  15618  cnplimcim  15661  cnlimci  15667  reeff1olem  15765  efltlemlt  15768  pellexlem1  15974  zabsle1  16001  lgslem3  16004  lgsmod  16028  lgsdir2lem5  16034  lgsdir2  16035  lgsne0  16040  lgsdirnn0  16049  gausslemma2dlem0f  16056  gausslemma2dlem1a  16060  gausslemma2dlem3  16065  2lgslem1c  16092  2lgslem3a1  16099  2lgslem3b1  16100  2lgslem3c1  16101  2lgslem3d1  16102  2lgslem3  16103  2lgsoddprmlem2  16108  uhgrm  16202  incistruhgr  16214  upgrfnen  16222  umgrfnen  16232  umgrnloop  16240  upgredgpr  16273  usgrausgrben  16296  usgredgop  16297  usgruspgrben  16310  usgrislfuspgrdom  16314  umgrvad2edg  16335  ushgredgedg  16350  ushgredgedgloop  16352  uhgr0v0e  16358  subgreldmiedg  16393  subupgr  16397  uhgrspansubgrlem  16400  vtxdg0v  16418  wlkpropg  16448  wlkvg  16452  wlkl1loop  16482  upgriswlkdc  16484  upgrwlkedg  16485  upgrwlkvtxedg  16488  uspgr2wlkeq  16489  wlkres  16503  trlf1  16512  clwwlk1loop  16523  clwwlkccatlem  16524  isclwwlknx  16540  clwwlkn1loopb  16544  clwwlkext2edg  16546  umgr2cwwk2dif  16548  clwwlknonex2lem2  16562  clwwlknonex2  16563  eupthseg  16576  eupth2lem3lem4fi  16597  bj-charfun  16716  bj-charfunr  16719  bj-charfunbi  16720  bj-prexg  16820  peano5set  16849  bj-peano4  16864  bj-nn0suc  16873  bj-nn0sucALT  16887  bj-findis  16888  exmidsbthrlem  16941  trilpolemres  16965  trirec0  16967  nconstwlpolem  16990  neapmkv  16993