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  558  anabsi5  579  anim12dan  602  pm3.43  604  con3dimp  638  annimim  690  imnan  694  jaoian  799  jaodan  801  stdcndc  849  impidc  862  pm2.5gdc  870  con2bidc  879  pm5.18dc  887  dfandc  888  pm4.63dc  890  pm4.54dc  906  pm4.79dc  907  orcanai  932  annimdc  942  pm4.55dc  943  orandc  944  pm4.82  955  pm3.11dc  962  pm3.12dc  963  dn1dc  965  3jcad  1183  3expia  1210  3an1rs  1224  3imp1  1225  3imp2  1227  syl3anl2  1301  3jaoian  1320  3jaodan  1321  mp3anl1  1346  mp3anl2  1347  mp3anl3  1348  ecased  1364  xor3dc  1409  pm5.15dc  1411  xor2dc  1412  xornbidc  1413  xordc  1414  nbbndc  1416  biassdc  1417  bilukdc  1418  dfbi3dc  1419  pm5.24dc  1420  xordidc  1421  alanimi  1485  19.29  1646  equs4  1751  equsexd  1755  spimth  1761  equs5a  1820  ax11v2  1846  ax11b  1852  equs5or  1856  sb5rf  1878  equvin  1889  nfsb4t  2045  eu5  2105  mopick  2136  euexex  2143  2euswapdc  2149  exists2  2155  eqrdav  2208  dvelimdc  2373  nebidc  2460  pm13.18  2461  nelne1  2470  nelne2  2471  rspa  2558  ralrimdvv  2594  r19.21bi  2598  r19.26  2637  ralbi  2643  rexbi  2644  r19.29  2648  vtoclgft  2831  rspcva  2885  rspc2va  2901  elabgt  2924  eqeu  2953  mob2  2963  mob  2965  euind  2970  reu6  2972  reuind  2988  sbctt  3075  rspsbca  3093  sbcnestgf  3156  rspcsbela  3164  ssel2  3199  sselda  3204  sstr  3212  nssne1  3262  nssne2  3263  reuss2  3464  reupick  3468  reupick2  3470  reximdva0m  3487  ssn0  3514  disjel  3526  ssdisj  3528  absneu  3718  preqr1g  3823  prel12  3828  dfiun2g  3976  nbrne1  4081  nbrne2  4082  mpteq12f  4143  triun  4174  csbexga  4191  iinexgm  4217  prexg  4274  copsex2t  4310  swopo  4374  poirr  4375  potr  4376  pofun  4380  issod  4387  ordelss  4447  trssord  4448  limelon  4467  trsuc  4490  eusvnfb  4522  rabxfrd  4537  regexmidlem1  4602  nordeq  4613  suc11g  4626  nnsuc  4685  brrelex12  4734  vtoclr  4744  optocl  4772  relop  4849  brcogw  4868  breldmg  4906  elreldm  4926  riinint  4961  issref  5087  xpidtr  5095  trin2  5096  cnveqb  5160  funopg  5328  funssres  5336  fununi  5365  funimass2  5375  imain  5379  fnun  5405  fco  5465  opelf  5472  f0rn0  5496  f1oun  5568  fun11iun  5569  fv3  5626  ndmfvg  5634  fvelima  5658  fvopab3ig  5681  fvmptssdm  5692  fvmptf  5700  fvimacnv  5723  fmptco  5774  funfvima2  5845  funfvima3  5846  f1veqaeq  5866  f1ocnvfvrneq  5879  fliftfun  5893  isotr  5913  isoini  5915  isopolem  5919  isosolem  5921  moriotass  5958  acexmidlem2  5971  suppssfv  6184  suppssov1  6185  f1dmex  6231  releldm2  6301  f1o2ndf1  6344  poxp  6348  tposf2  6384  iunon  6400  smoel2  6419  tfrlem9  6435  tfrexlem  6450  tfr1onlembxssdm  6459  tfr1onlemres  6465  tfrcllembxssdm  6472  tfrcllemres  6478  tfrcl  6480  tfri3  6483  frecabcl  6515  sucinc2  6562  nnacom  6600  nnmcom  6605  nnsucsssuc  6608  nnsucuniel  6611  nntri2or2  6614  nnaordi  6624  nnmordi  6632  nnaordex  6644  nnm00  6646  ectocld  6718  iinerm  6724  th3qlem2  6755  elpm2r  6783  mapsncnv  6812  mptelixpg  6851  ixpsnf1o  6853  f1oen4g  6873  f1dom4g  6874  f1oen3g  6875  f1oeng  6878  en2d  6889  en3d  6890  dom2lem  6893  fundmen  6929  fundmeng  6930  unen  6939  rex2dom  6941  en2m  6944  xpdom2  6958  xpdom2g  6959  fopwdom  6965  nneneq  6986  phpm  6995  phpelm  6996  dif1enen  7010  fin0  7015  findcard  7018  diffifi  7024  ac6sfi  7028  onunsnss  7047  fiintim  7061  xpfi  7062  infidc  7069  fidcenum  7091  sbthlem1  7092  sbthlemi3  7094  sbthlemi10  7101  elfir  7108  isotilem  7141  inflbti  7159  ordiso2  7170  eldju2ndl  7207  eldju2ndr  7208  updjudhf  7214  mkvprop  7293  carden2bex  7330  pm54.43  7331  exmidfodomrlemeldju  7345  exmidfodomrlemreseldju  7346  exmidfodomrlemim  7347  pw1m  7377  ltmpig  7494  enq0sym  7587  addnq0mo  7602  mulnq0mo  7603  prarloclem3step  7651  prarloclem3  7652  genpml  7672  genpmu  7673  genprndl  7676  genprndu  7677  genpdisj  7678  distrlem1prl  7737  distrlem1pru  7738  distrlem4prl  7739  distrlem4pru  7740  distrlem5prl  7741  distrlem5pru  7742  ltsopr  7751  ltaddpr  7752  addcanprleml  7769  addcanprlemu  7770  recexprlemm  7779  recexprlemlol  7781  recexprlemupu  7783  aptiprleml  7794  aptiprlemu  7795  caucvgprlemnkj  7821  caucvgprlemnbj  7822  addsrmo  7898  mulsrmo  7899  srpospr  7938  caucvgsr  7957  axprecex  8035  mpomulf  8104  mulgt0  8189  ltne  8199  cnegexlem1  8289  cnegexlem2  8290  negf1o  8496  addgt0  8563  addgegt0  8564  addgtge0  8565  addge0  8566  recexre  8693  mulge0  8734  recexap  8768  prodgt02  8968  prodge02  8970  ltmul12a  8975  mulgt1  8978  nndivtr  9120  addltmul  9316  elnnnn0b  9381  xnn0nnn0pnf  9413  elnnz  9424  zmulcl  9468  nn0n0n1ge2  9485  nn0lt2  9496  nn0le2is012  9497  uzind2  9527  nn0ind-raph  9532  eluzp1m1  9714  uz3m2nn  9736  supinfneg  9758  infsupneg  9759  infregelbex  9761  negm  9778  lbzbi  9779  qaddcl  9798  qmulcl  9800  qreccl  9805  elpq  9812  ledivge1le  9890  nn0ledivnn  9931  xrltne  9977  xrre  9984  xrre2  9985  xrre3  9986  ge0gtmnf  9987  xltnegi  9999  xnn0xadd0  10031  xnegdi  10032  xposdif  10046  xlesubadd  10047  iccsupr  10130  icoshft  10154  icoshftf1o  10155  fznlem  10205  fzen  10207  uzsubsubfz  10211  fzsuc2  10243  elfz1b  10254  elfz0ubfz0  10289  elfz0fzfz0  10290  fz0fzelfz0  10291  fz0fzdiffz0  10294  elfzmlbp  10296  difelfznle  10299  fzofzim  10356  elincfzoext  10366  eluzgtdifelfzo  10370  elfzodifsumelfzo  10374  elfzonlteqm1  10383  elfzom1p1elfzo  10387  ssfzo12bi  10398  subfzo0  10415  zsupcllemex  10417  zssinfcl  10419  exbtwnzlemstep  10434  modqmuladdnn0  10557  modfzo0difsn  10584  addmodlteq  10587  frec2uzlt2d  10593  frecuzrdgtcl  10601  frecuzrdgfunlem  10608  seqf1og  10710  m1expcl2  10750  expge1  10765  leexp2r  10782  expubnd  10785  zesq  10847  expnlbnd  10853  nn0ltexp2  10898  nn0opthd  10911  faclbnd  10930  bcpasc  10955  hashprg  10997  seq3coll  11031  wrdnval  11068  wrdsymb0  11070  fstwrdne  11076  wrdred1hash  11081  swrdnd  11157  swrdwrdsymbg  11162  swrdsbslen  11164  swrdlsw  11167  swrdswrdlem  11202  swrdswrd  11203  pfxswrd  11204  cats1un  11219  wrd2ind  11221  swrdccatin1  11223  pfxccatin12lem4  11224  pfxccatin12lem2a  11225  pfxccatin12lem1  11226  swrdccatin2  11227  pfxccatin12lem2c  11228  pfxccatin12lem2  11229  pfxccatin12lem3  11230  pfxccatin12  11231  pfxccat3  11232  swrdccat  11233  pfxccat3a  11236  swrdccat3blem  11237  swrdccat3b  11238  swrdccatin2d  11242  reuccatpfxs1lem  11244  rexanuz  11465  rexuz3  11467  r19.29uz  11469  r19.2uz  11470  absnid  11550  leabs  11551  ltabs  11564  icodiamlt  11657  maxleast  11690  negfi  11705  climcn2  11786  climcau  11824  climcaucn  11828  sumdc  11835  fsum3cvg  11855  isumz  11866  fsumf1o  11867  fisumss  11869  isumss2  11870  fsumzcl2  11882  fsumsplit  11884  fsumsplitsnun  11896  sumsplitdc  11909  fsum2dlemstep  11911  telfsumo  11943  fsumparts  11947  fsumiun  11954  isumrpcl  11971  fproddccvg  12049  prod1dc  12063  prodssdc  12066  fprodssdc  12067  prodsnf  12069  fprodsplitdc  12073  fprod2dlemstep  12099  fprodmodd  12118  efexp  12159  efieq1re  12249  p1modz1  12271  dvds0lem  12278  dvds2ln  12301  dvdssub2  12312  dvdsadd2b  12317  dvdsabseq  12324  divconjdvds  12326  dvdsdivcl  12327  odd2np1  12350  oddge22np1  12358  opoe  12372  omoe  12373  opeo  12374  omeo  12375  m1expo  12377  nn0ehalf  12380  nn0o1gt2  12382  nno  12383  divalgb  12402  ndvdsadd  12408  bitsinv1lem  12438  gcd0id  12466  gcdneg  12469  gcdaddm  12471  bezoutlemstep  12484  dfgcd2  12501  gcddiv  12506  dvdsmulgcd  12512  bezoutr  12519  bezoutr1  12520  uzwodc  12524  nninfctlemfo  12527  algfx  12540  lcmgcdlem  12565  lcmgcdeq  12571  coprmdvds  12580  divgcdcoprmex  12590  cncongr1  12591  cncongr2  12592  isprm3  12606  dvdsnprmd  12613  prmgt1  12620  oddprmgt2  12622  isprm6  12635  cncongrprm  12645  phibndlem  12704  phimullem  12713  powm2modprm  12741  modprm0  12743  modprmn0modprm0  12745  prm23lt5  12752  pcneg  12814  pcprmpw2  12822  dvdsprmpweqnn  12825  dvdsprmpweqle  12826  pcaddlem  12828  fldivp1  12837  pcfac  12839  oddprmdvds  12843  prmunb  12851  ennnfone  12962  unct  12979  lidrididd  13381  gsummgmpropd  13393  sgrpass  13407  issgrpd  13411  issubmnd  13441  imasmnd2  13451  mnd1id  13455  insubm  13484  dfgrp2  13526  grpid  13538  grpasscan1  13562  dfgrp3mlem  13597  dfgrp3me  13599  imasgrp2  13613  mulgnn0gsum  13631  mulgnn0p1  13636  mulgaddcom  13649  mulginvcom  13650  mulgass  13662  mulgpropdg  13667  subginv  13684  issubg2m  13692  issubg4m  13696  grpissubg  13697  resgrpisgrp  13698  subgintm  13701  kerf1ghm  13777  cmncom  13805  imasabl  13839  rngdi  13869  rngdir  13870  rngpropd  13884  imasrng  13885  imasring  13993  nzrunit  14117  issubrng2  14139  subrngintm  14141  issubrg2  14170  subrgintm  14172  lmodfopnelem1  14253  lmodfopnelem2  14254  lmodfopne  14255  islssm  14286  islidlm  14408  rnglidlmcl  14409  dflidl2rng  14410  rnglidlmmgm  14425  rnglidlmsgrp  14426  rnglidlrng  14427  dvdsrzring  14532  znidom  14586  uniopn  14640  istopon  14652  fiinbas  14688  tg2  14699  tgcl  14703  0nnei  14792  tgrest  14808  tgcn  14847  cnpnei  14858  cncnp2m  14870  lmtopcnp  14889  tx2cn  14909  txcn  14914  cnmpt21  14930  isxmet2d  14987  metrest  15145  metcnpi3  15156  tgioo  15193  fsumcncntop  15206  elcncf1di  15218  climcncf  15223  cncfco  15230  suplociccreex  15263  cnplimcim  15306  cnlimci  15312  reeff1olem  15410  efltlemlt  15413  zabsle1  15643  lgslem3  15646  lgsmod  15670  lgsdir2lem5  15676  lgsdir2  15677  lgsne0  15682  lgsdirnn0  15691  gausslemma2dlem0f  15698  gausslemma2dlem1a  15702  gausslemma2dlem3  15707  2lgslem1c  15734  2lgslem3a1  15741  2lgslem3b1  15742  2lgslem3c1  15743  2lgslem3d1  15744  2lgslem3  15745  2lgsoddprmlem2  15750  uhgrm  15843  incistruhgr  15855  upgrfnen  15863  umgrfnen  15873  umgrnloop  15881  upgredgpr  15912  usgrausgrben  15935  usgredgop  15936  usgruspgrben  15949  usgrislfuspgrdom  15953  umgrvad2edg  15974  ushgredgedg  15989  ushgredgedgloop  15991  bj-charfun  16080  bj-charfunr  16083  bj-charfunbi  16084  bj-prexg  16184  peano5set  16213  bj-peano4  16228  bj-nn0suc  16237  bj-nn0sucALT  16251  bj-findis  16252  exmidsbthrlem  16301  trilpolemres  16321  trirec0  16323  nconstwlpolem  16344  neapmkv  16347