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  1772  equsexd  1776  spimth  1782  equs5a  1841  ax11v2  1867  ax11b  1873  equs5or  1877  sb5rf  1899  equvin  1910  nfsb4t  2066  eu5  2126  mopick  2157  euexex  2164  2euswapdc  2170  exists2  2176  eqrdav  2229  dvelimdc  2394  nebidc  2481  pm13.18  2482  nelne1  2491  nelne2  2492  rspa  2579  ralrimdvv  2615  r19.21bi  2619  r19.26  2658  ralbi  2664  rexbi  2665  r19.29  2669  vtoclgft  2853  rspcva  2907  rspc2va  2923  elabgt  2946  eqeu  2975  mob2  2985  mob  2987  euind  2992  reu6  2994  reuind  3010  sbctt  3097  rspsbca  3115  sbcnestgf  3178  rspcsbela  3186  ssel2  3221  sselda  3226  sstr  3234  nssne1  3284  nssne2  3285  reuss2  3486  reupick  3490  reupick2  3492  reximdva0m  3509  ssn0  3536  disjel  3548  ssdisj  3550  absneu  3744  preqr1g  3850  prel12  3855  dfiun2g  4003  nbrne1  4108  nbrne2  4109  mpteq12f  4170  triun  4201  csbexga  4218  prcssprc  4231  iinexgm  4245  prexg  4303  copsex2t  4339  swopo  4405  poirr  4406  potr  4407  pofun  4411  issod  4418  ordelss  4478  trssord  4479  limelon  4498  trsuc  4521  eusvnfb  4553  rabxfrd  4568  regexmidlem1  4633  nordeq  4644  suc11g  4657  nnsuc  4716  brrelex12  4766  vtoclr  4776  optocl  4804  relop  4882  brcogw  4901  breldmg  4939  elreldm  4960  riinint  4995  issref  5121  xpidtr  5129  trin2  5130  cnveqb  5194  funopg  5362  funssres  5371  fununi  5400  funimass2  5410  imain  5414  fnun  5440  fco  5502  opelf  5509  f0rn0  5534  f1oun  5606  fun11iun  5607  fv3  5665  ndmfvg  5673  fvelima  5700  fvopab3ig  5723  fvmptssdm  5734  fvmptf  5742  fvimacnv  5765  fmptco  5816  fcof  5836  funfvima2  5892  funfvima3  5893  f1veqaeq  5915  f1ocnvfvrneq  5928  fliftfun  5942  isotr  5962  isoini  5964  isopolem  5968  isosolem  5970  moriotass  6007  acexmidlem2  6020  suppssfv  6236  suppssov1  6237  f1dmex  6283  releldm2  6353  f1o2ndf1  6398  poxp  6402  tposf2  6439  iunon  6455  smoel2  6474  tfrlem9  6490  tfrexlem  6505  tfr1onlembxssdm  6514  tfr1onlemres  6520  tfrcllembxssdm  6527  tfrcllemres  6533  tfrcl  6535  tfri3  6538  frecabcl  6570  sucinc2  6619  nnacom  6657  nnmcom  6662  nnsucsssuc  6665  nnsucuniel  6668  nntri2or2  6671  nnaordi  6681  nnmordi  6689  nnaordex  6701  nnm00  6703  ectocld  6775  iinerm  6781  th3qlem2  6812  elpm2r  6840  mapsncnv  6869  mptelixpg  6908  ixpsnf1o  6910  f1oen4g  6930  f1dom4g  6931  f1oen3g  6932  f1oeng  6935  en2d  6946  en3d  6947  dom2lem  6950  fundmen  6986  fundmeng  6987  unen  6996  modom  6999  rex2dom  7001  en2m  7004  xpdom2  7020  xpdom2g  7021  fopwdom  7027  nneneq  7048  phpm  7057  phpelm  7058  dif1enen  7074  fin0  7079  findcard  7082  diffifi  7088  ac6sfi  7092  onunsnss  7114  fiintim  7128  xpfi  7129  infidc  7138  fidcenum  7160  sbthlem1  7161  sbthlemi3  7163  sbthlemi10  7170  elfir  7177  isotilem  7210  inflbti  7228  ordiso2  7239  eldju2ndl  7276  eldju2ndr  7277  updjudhf  7283  mkvprop  7362  carden2bex  7399  pm54.43  7400  exmidfodomrlemeldju  7415  exmidfodomrlemreseldju  7416  exmidfodomrlemim  7417  pw1m  7447  ltmpig  7564  enq0sym  7657  addnq0mo  7672  mulnq0mo  7673  prarloclem3step  7721  prarloclem3  7722  genpml  7742  genpmu  7743  genprndl  7746  genprndu  7747  genpdisj  7748  distrlem1prl  7807  distrlem1pru  7808  distrlem4prl  7809  distrlem4pru  7810  distrlem5prl  7811  distrlem5pru  7812  ltsopr  7821  ltaddpr  7822  addcanprleml  7839  addcanprlemu  7840  recexprlemm  7849  recexprlemlol  7851  recexprlemupu  7853  aptiprleml  7864  aptiprlemu  7865  caucvgprlemnkj  7891  caucvgprlemnbj  7892  addsrmo  7968  mulsrmo  7969  srpospr  8008  caucvgsr  8027  axprecex  8105  mpomulf  8174  mulgt0  8259  ltne  8269  cnegexlem1  8359  cnegexlem2  8360  negf1o  8566  addgt0  8633  addgegt0  8634  addgtge0  8635  addge0  8636  recexre  8763  mulge0  8804  recexap  8838  prodgt02  9038  prodge02  9040  ltmul12a  9045  mulgt1  9048  nndivtr  9190  addltmul  9386  elnnnn0b  9451  xnn0nnn0pnf  9483  elnnz  9494  zmulcl  9538  nn0n0n1ge2  9555  nn0lt2  9566  nn0le2is012  9567  uzind2  9597  nn0ind-raph  9602  eluzp1m1  9785  uz3m2nn  9812  supinfneg  9834  infsupneg  9835  infregelbex  9837  negm  9854  lbzbi  9855  qaddcl  9874  qmulcl  9876  qreccl  9881  elpq  9888  ledivge1le  9966  nn0ledivnn  10007  xrltne  10053  xrre  10060  xrre2  10061  xrre3  10062  ge0gtmnf  10063  xltnegi  10075  xnn0xadd0  10107  xnegdi  10108  xposdif  10122  xlesubadd  10123  iccsupr  10206  icoshft  10230  icoshftf1o  10231  fznlem  10281  fzen  10283  uzsubsubfz  10287  fzsuc2  10319  elfz1b  10330  elfz0ubfz0  10365  elfz0fzfz0  10366  fz0fzelfz0  10367  fz0fzdiffz0  10370  elfzmlbp  10372  difelfznle  10375  nn0p1elfzo  10427  fzofzim  10433  elincfzoext  10444  eluzgtdifelfzo  10448  elfzodifsumelfzo  10452  elfzonlteqm1  10461  elfzom1p1elfzo  10465  ssfzo12bi  10476  subfzo0  10494  zsupcllemex  10496  zssinfcl  10498  exbtwnzlemstep  10513  modqmuladdnn0  10636  modfzo0difsn  10663  addmodlteq  10666  frec2uzlt2d  10672  frecuzrdgtcl  10680  frecuzrdgfunlem  10687  seqf1og  10789  m1expcl2  10829  expge1  10844  leexp2r  10861  expubnd  10864  zesq  10926  expnlbnd  10932  nn0ltexp2  10977  nn0opthd  10990  faclbnd  11009  bcpasc  11034  hashprg  11078  seq3coll  11112  wrdnval  11153  wrdsymb0  11155  fstwrdne  11161  wrdred1hash  11166  swrdnd  11249  swrdwrdsymbg  11254  swrdsbslen  11256  swrdlsw  11259  swrdswrdlem  11294  swrdswrd  11295  pfxswrd  11296  cats1un  11311  wrd2ind  11313  swrdccatin1  11315  pfxccatin12lem4  11316  pfxccatin12lem2a  11317  pfxccatin12lem1  11318  swrdccatin2  11319  pfxccatin12lem2c  11320  pfxccatin12lem2  11321  pfxccatin12lem3  11322  pfxccatin12  11323  pfxccat3  11324  swrdccat  11325  pfxccat3a  11328  swrdccat3blem  11329  swrdccat3b  11330  swrdccatin2d  11334  reuccatpfxs1lem  11336  rexanuz  11571  rexuz3  11573  r19.29uz  11575  r19.2uz  11576  absnid  11656  leabs  11657  ltabs  11670  icodiamlt  11763  maxleast  11796  negfi  11811  climcn2  11892  climcau  11930  climcaucn  11934  sumdc  11941  fsum3cvg  11962  isumz  11973  fsumf1o  11974  fisumss  11976  isumss2  11977  fsumzcl2  11989  fsumsplit  11991  fsumsplitsnun  12003  sumsplitdc  12016  fsum2dlemstep  12018  telfsumo  12050  fsumparts  12054  fsumiun  12061  isumrpcl  12078  fproddccvg  12156  prod1dc  12170  prodssdc  12173  fprodssdc  12174  prodsnf  12176  fprodsplitdc  12180  fprod2dlemstep  12206  fprodmodd  12225  efexp  12266  efieq1re  12356  p1modz1  12378  dvds0lem  12385  dvds2ln  12408  dvdssub2  12419  dvdsadd2b  12424  dvdsabseq  12431  divconjdvds  12433  dvdsdivcl  12434  odd2np1  12457  oddge22np1  12465  opoe  12479  omoe  12480  opeo  12481  omeo  12482  m1expo  12484  nn0ehalf  12487  nn0o1gt2  12489  nno  12490  divalgb  12509  ndvdsadd  12515  bitsinv1lem  12545  gcd0id  12573  gcdneg  12576  gcdaddm  12578  bezoutlemstep  12591  dfgcd2  12608  gcddiv  12613  dvdsmulgcd  12619  bezoutr  12626  bezoutr1  12627  uzwodc  12631  nninfctlemfo  12634  algfx  12647  lcmgcdlem  12672  lcmgcdeq  12678  coprmdvds  12687  divgcdcoprmex  12697  cncongr1  12698  cncongr2  12699  isprm3  12713  dvdsnprmd  12720  prmgt1  12727  oddprmgt2  12729  isprm6  12742  cncongrprm  12752  phibndlem  12811  phimullem  12820  powm2modprm  12848  modprm0  12850  modprmn0modprm0  12852  prm23lt5  12859  pcneg  12921  pcprmpw2  12929  dvdsprmpweqnn  12932  dvdsprmpweqle  12933  pcaddlem  12935  fldivp1  12944  pcfac  12946  oddprmdvds  12950  prmunb  12958  ennnfone  13069  unct  13086  lidrididd  13488  gsummgmpropd  13500  sgrpass  13514  issgrpd  13518  issubmnd  13548  imasmnd2  13558  mnd1id  13562  insubm  13591  dfgrp2  13633  grpid  13645  grpasscan1  13669  dfgrp3mlem  13704  dfgrp3me  13706  imasgrp2  13720  mulgnn0gsum  13738  mulgnn0p1  13743  mulgaddcom  13756  mulginvcom  13757  mulgass  13769  mulgpropdg  13774  subginv  13791  issubg2m  13799  issubg4m  13803  grpissubg  13804  resgrpisgrp  13805  subgintm  13808  kerf1ghm  13884  cmncom  13912  imasabl  13946  rngdi  13977  rngdir  13978  rngpropd  13992  imasrng  13993  imasring  14101  nzrunit  14226  issubrng2  14248  subrngintm  14250  issubrg2  14279  subrgintm  14281  lmodfopnelem1  14362  lmodfopnelem2  14363  lmodfopne  14364  islssm  14395  islidlm  14517  rnglidlmcl  14518  dflidl2rng  14519  rnglidlmmgm  14534  rnglidlmsgrp  14535  rnglidlrng  14536  dvdsrzring  14641  znidom  14695  uniopn  14754  istopon  14766  fiinbas  14802  tg2  14813  tgcl  14817  0nnei  14906  tgrest  14922  tgcn  14961  cnpnei  14972  cncnp2m  14984  lmtopcnp  15003  tx2cn  15023  txcn  15028  cnmpt21  15044  isxmet2d  15101  metrest  15259  metcnpi3  15270  tgioo  15307  fsumcncntop  15320  elcncf1di  15332  climcncf  15337  cncfco  15344  suplociccreex  15377  cnplimcim  15420  cnlimci  15426  reeff1olem  15524  efltlemlt  15527  zabsle1  15757  lgslem3  15760  lgsmod  15784  lgsdir2lem5  15790  lgsdir2  15791  lgsne0  15796  lgsdirnn0  15805  gausslemma2dlem0f  15812  gausslemma2dlem1a  15816  gausslemma2dlem3  15821  2lgslem1c  15848  2lgslem3a1  15855  2lgslem3b1  15856  2lgslem3c1  15857  2lgslem3d1  15858  2lgslem3  15859  2lgsoddprmlem2  15864  uhgrm  15958  incistruhgr  15970  upgrfnen  15978  umgrfnen  15988  umgrnloop  15996  upgredgpr  16029  usgrausgrben  16052  usgredgop  16053  usgruspgrben  16066  usgrislfuspgrdom  16070  umgrvad2edg  16091  ushgredgedg  16106  ushgredgedgloop  16108  uhgr0v0e  16114  subgreldmiedg  16149  subupgr  16153  uhgrspansubgrlem  16156  vtxdg0v  16174  wlkpropg  16204  wlkvg  16208  wlkl1loop  16238  upgriswlkdc  16240  upgrwlkedg  16241  upgrwlkvtxedg  16244  uspgr2wlkeq  16245  wlkres  16259  trlf1  16268  clwwlk1loop  16279  clwwlkccatlem  16280  isclwwlknx  16296  clwwlkn1loopb  16300  clwwlkext2edg  16302  umgr2cwwk2dif  16304  clwwlknonex2lem2  16318  clwwlknonex2  16319  eupthseg  16332  eupth2lem3lem4fi  16353  bj-charfun  16462  bj-charfunr  16465  bj-charfunbi  16466  bj-prexg  16566  peano5set  16595  bj-peano4  16610  bj-nn0suc  16619  bj-nn0sucALT  16633  bj-findis  16634  exmidsbthrlem  16689  trilpolemres  16713  trirec0  16715  nconstwlpolem  16737  neapmkv  16740  gfsumval  16748