MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  impcom Structured version   Visualization version   GIF version

Theorem impcom 408
Description: Importation inference with commuted antecedents. (Contributed by NM, 25-May-2005.)
Hypothesis
Ref Expression
imp.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
impcom ((𝜓𝜑) → 𝜒)

Proof of Theorem impcom
StepHypRef Expression
1 imp.1 . . 3 (𝜑 → (𝜓𝜒))
21com12 32 . 2 (𝜓 → (𝜑𝜒))
32imp 407 1 ((𝜓𝜑) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 208  df-an 397
This theorem is referenced by:  mpan9  507  bianir  1050  19.29r  1866  19.41v  1941  19.41  2228  nfsb4t  2535  nfsb4tALT  2600  mo4  2646  2euexv  2712  2euex  2722  gencl  3535  2gencl  3536  vtocl2ga  3575  vtocl4g  3579  rspccva  3621  2reurex  3749  2reu1  3880  rexdifi  4121  sseq0  4352  r19.2z  4438  falseral0  4457  elelpwi  4552  preqsnd  4783  prproe  4830  ssuni  4854  disji2  5040  invdisjrab  5044  disjiun  5045  disjxiun  5055  trintss  5181  ssexg  5219  reusv2lem3  5292  propeqop  5389  otiunsndisj  5402  rexopabb  5407  pofun  5485  solin  5492  2optocl  5640  3optocl  5641  ssrelrn  5757  elrnmpt1  5824  resieq  5858  reuop  6138  funimaexg  6434  fnun  6457  fss  6521  fun  6534  fvelimab  6731  fvmptss  6773  fvn0ssdmfun  6835  fvcofneq  6852  fmptco  6884  funsndifnop  6906  fnressn  6913  fressnfv  6915  fvn0fvelrn  6918  fmptsng  6923  fvtp2g  6954  fvtp3g  6955  tpres  6956  fnex  6972  funfvima3  6989  isores3  7077  dmfex  7629  opreuopreu  7725  releldmdifi  7735  funeldmdif  7738  el2mpocsbcl  7771  f1o2ndf1  7809  frxp  7811  fnse  7818  ressuppssdif  7842  funsssuppss  7847  suppss  7851  mpoxopxnop0  7872  reldmtpos  7891  wfrfun  7956  wfrlem12  7957  smores  7980  tfrlem7  8010  tz7.48-2  8069  tz7.49  8072  oacl  8151  omcl  8152  oecl  8153  oarec  8178  oewordri  8208  oeworde  8209  oelim2  8211  oeoa  8213  oeoelem  8214  oeoe  8215  nnacl  8227  nnmcl  8228  nnecl  8229  nnmsucr  8241  2ecoptocl  8378  undifixp  8487  ssct  8587  xpf1o  8668  limensuc  8683  ac6sfi  8751  frfi  8752  difinf  8777  f1dmvrnfibi  8797  f1vrnfibi  8798  suppeqfsuppbi  8836  elfiun  8883  dffi3  8884  infsupprpr  8957  xpwdomg  9038  infdiffi  9110  epfrs  9162  rankxpsuc  9300  updjud  9352  tskwe  9368  infxpenlem  9428  fseqenlem1  9439  kmlem2  9566  cff1  9669  cflim2  9674  sornom  9688  infpssrlem4  9717  fin23lem26  9736  fin23lem30  9753  fin23lem34  9757  isf32lem11  9774  fin67  9806  isfin7-2  9807  fin1a2lem10  9820  axcc2lem  9847  axdc2lem  9859  axdc3lem2  9862  axdc3lem4  9864  axdc4lem  9866  iunfo  9950  tsk0  10174  gruina  10229  grur1a  10230  mulcanenq  10371  reclem2pr  10459  supsrlem  10522  supsr  10523  ax1rid  10572  negf1o  11059  mulgt1  11488  fiminreOLD  11579  lbreu  11580  nnaddcl  11649  nnmulcl  11650  nn0n0n1ge2b  11952  nn0indd  12068  fzind  12069  fnn0ind  12070  uzaddcl  12293  uzinfi  12317  nn01to3  12330  elpq  12364  xmulasslem2  12665  supxrunb1  12702  supxrunb2  12703  infmremnf  12726  infmrp1  12727  uzsubsubfz  12919  elfz0ubfz0  13001  fz0fzdiffz0  13006  elfzmlbp  13008  fzofzim  13074  elfzom1elp1fzo  13094  ssfzo12bi  13122  fzonfzoufzol  13130  elfznelfzob  13133  injresinjlem  13147  injresinj  13148  modaddmodup  13292  modfzo0difsn  13301  modsumfzodifsn  13302  addmodlteq  13304  om2uzlti  13308  fsequb  13333  ssnn0fi  13343  ser1const  13416  expcllem  13430  expeq0  13449  expmordi  13521  expnngt1  13592  faclbnd  13640  hashf1rn  13703  hashgadd  13728  hashunx  13737  hashnn0n0nn  13742  hashgt0elex  13752  hashss  13760  hashfzp1  13782  hashxp  13785  hashmap  13786  hashimarni  13792  seqcoll  13812  hash2exprb  13819  hashge2el2difr  13829  elss2prb  13835  hashdifsnp1  13844  fi1uzind  13845  brfi1indALT  13848  lswlgt0cl  13911  swrdnd  14006  swrdnnn0nd  14008  swrdnd0  14009  swrd0  14010  swrdsbslen  14016  swrdspsleq  14017  pfxsuff1eqwrdeq  14051  swrdswrdlem  14056  swrdswrd  14057  wrd2ind  14075  pfxccatin12lem2a  14079  swrdccatin2  14081  pfxccatin12lem2  14083  pfxccatin12lem3  14084  pfxccatin12  14085  pfxccat3  14086  swrdccat  14087  pfxccat3a  14090  swrdccat3blem  14091  repswswrd  14136  repswrevw  14139  cshwmodn  14147  cshwsublen  14148  cshwidxmod  14155  cshwidxmodr  14156  cshf1  14162  2cshw  14165  cshweqrep  14173  cshw1  14174  2cshwcshw  14177  cshwcshid  14179  cshwcsh2id  14180  wrdlen2i  14294  2swrd2eqwrdeq  14305  wwlktovfo  14312  relexpsucnnl  14381  rtrclreclem3  14409  rtrclreclem4  14410  relexpindlem  14412  r19.29uz  14700  caubnd  14708  sqreu  14710  climshft  14923  climub  15008  climserle  15009  sumss  15071  sumss2  15073  modfsummods  15138  o1fsum  15158  binom  15175  climcndslem1  15194  climcndslem2  15195  pwm1geoserOLD  15215  cvgrat  15229  clim2prod  15234  prodfn0  15240  prodfrec  15241  ntrivcvgfvn0  15245  fprodn0  15323  fprodmodd  15341  fprodefsum  15438  demoivreALT  15544  ruclem8  15580  dvdsaddre2b  15647  dvdsdivcl  15656  dvdsfac  15666  oddnn02np1  15687  oddge22np1  15688  evennn02n  15689  evennn2n  15690  m1exp1  15717  nn0o  15724  pwp1fsum  15732  flodddiv4  15754  smu01lem  15824  dvdslegcd  15843  gcdneg  15860  dfgcd2  15884  gcdmultipleOLD  15890  seq1st  15905  alginv  15909  lcmf  15967  lcmftp  15970  lcmfunsnlem2lem2  15973  lcmfunsnlem  15975  lcmfun  15979  ncoprmgcdne1b  15984  coprmproddvdslem  15996  coprmproddvds  15997  cncongr1  16001  prmdvdsexp  16049  prmndvdsfaclt  16057  ncoprmlnprm  16058  fvprmselgcd1  16371  prmgaplem6  16382  prmgaplem7  16383  prmgaplem8  16384  cshwshashlem1  16419  setsstruct2  16511  setsstruct  16513  inveq  17034  catsubcat  17099  initoeu2lem0  17263  initoeu2lem1  17264  funcestrcsetclem8  17387  funcestrcsetclem9  17388  fthestrcsetc  17390  fullestrcsetc  17391  funcsetcestrclem9  17403  fthsetcestrc  17405  fullsetcestrc  17406  lubss  17721  lubel  17722  issstrmgm  17853  mgmb1mgm1  17855  sgrpidmnd  17906  frmdgsum  18017  mgm2nsgrplem3  18025  dfgrp2  18068  cyccom  18286  gaass  18367  gsumwrev  18434  symgextf1lem  18479  symgextf1  18480  fvcosymgeq  18488  gsmsymgreq  18491  symgfixelsi  18494  pmtrprfv3  18513  symggen  18529  pmtrprfval  18546  gsumzres  18960  gsumpr  19006  gsumzunsnd  19007  srgmulgass  19212  srgbinom  19226  lmodvsmmulgdi  19600  lmodfopnelem1  19601  rmodislmodlem  19632  0ringnnzr  19972  assamulgscm  20060  gsumply1subr  20332  gsummoncoe1  20402  pf1ind  20448  cnfldmulg  20507  cnfldexp  20508  psgndiflemB  20674  matmulcell  20984  mat1dimscm  21014  dmatmul  21036  dmatscmcl  21042  scmataddcl  21055  scmatsubcl  21056  scmatsgrp1  21061  mavmulsolcl  21090  ma1repveval  21110  1marepvmarrepid  21114  symgmatr01lem  21192  slesolvec  21218  cramerimplem2  21223  decpmatmullem  21309  pm2mpf1  21337  mp2pm2mplem4  21347  monmat2matmon  21362  chpscmat  21380  chpscmatgsumbin  21382  fvmptnn04ifb  21389  chfacfscmul0  21396  chfacfscmulgsum  21398  chfacfpmmul0  21400  chfacfpmmulgsum  21402  cpmadugsumlemF  21414  toprntopon  21463  clsss  21592  ntrss  21593  restntr  21720  cmpsublem  21937  cmpsub  21938  2ndcrest  21992  txindislem  22171  t0kq  22356  filufint  22458  fbflim2  22515  flftg  22534  alexsubALTlem4  22588  cnextfvval  22603  ustuqtop4  22782  xmettri2  22879  mettri  22891  metss  23047  tngngp3  23194  clmvscom  23623  lmmbr  23790  caublcls  23841  lmcau  23845  ovolunlem1a  24026  nulmbl2  24066  voliunlem1  24080  iunmbl  24083  volsup  24086  dvlip  24519  dvfsumle  24547  degltlem1  24595  ply1divex  24659  plyco  24760  dgrnznn  24766  dvnply2  24805  plydivex  24815  aannenlem2  24847  aaliou3lem2  24861  ulmcau  24912  zabsle1  25800  gausslemma2dlem1a  25869  gausslemma2dlem2  25871  gausslemma2dlem3  25872  gausslemma2dlem4  25873  2lgslem1a1  25893  2sqnn0  25942  2sqreulem1  25950  2sqreunnlem1  25953  dchrisumlem1  25993  dchrisumlem2  25994  dchrisumlem3  25995  qabvle  26129  ostthlem2  26132  ostth2lem2  26138  tgjustr  26188  axeuclidlem  26676  incistruhgr  26792  umgredgprv  26820  umgrpredgv  26853  usgredgprvALT  26905  uhgr2edg  26918  usgredg2vlem2  26936  lfuhgr1v0e  26964  subgrfun  26991  umgrres1lem  27020  upgrres1  27023  fusgrfis  27040  uhgrnbgr0nb  27064  nbgr1vtx  27068  nb3grprlem1  27090  uvtx01vtx  27107  fusgrn0degnn0  27209  vtxdginducedm1lem4  27252  finsumvtxdg2size  27260  wlkl1loop  27347  wlkres  27380  lfgrwlknloop  27399  pthdadjvtx  27439  upgr2pthnlp  27441  upgrwlkdvdelem  27445  upgrwlkdvde  27446  uhgrwkspthlem2  27463  usgr2trlspth  27470  usgr2pth  27473  pthdlem2lem  27476  lfgrn1cycl  27511  uspgrn2crct  27514  crctcshwlkn0lem3  27518  crctcshwlkn0lem4  27519  crctcshwlkn0lem5  27520  iswspthsnon  27562  wlkiswwlks1  27573  wlklnwwlkln1  27574  wlkiswwlks2  27581  wlkiswwlksupgr2  27583  wlklnwwlkln2lem  27588  wlknwwlksnbij  27594  wwlksnred  27598  wwlksnext  27599  wwlksnredwwlkn  27601  wwlksnredwwlkn0  27602  wwlksnextfun  27604  wwlksnextinj  27605  wwlksnextsurj  27606  wspthsnonn0vne  27624  wspn0  27631  wwlks2onv  27660  elwwlks2  27673  elwspths2spth  27674  rusgrnumwwlk  27682  clwwlkccatlem  27695  clwlkclwwlklem2a1  27698  clwlkclwwlklem2fv2  27702  clwlkclwwlklem2a4  27703  clwlkclwwlklem2a  27704  clwlkclwwlklem2  27706  clwlkclwwlkf1lem3  27712  clwwisshclwwslem  27720  clwwisshclwwsn  27722  erclwwlktr  27728  isclwwlknx  27742  clwwlkinwwlk  27746  clwwlkel  27753  clwwlkf  27754  clwwlkf1  27756  clwwlkfo  27757  clwwlkext2edg  27763  wwlksext2clwwlk  27764  wwlksubclwwlk  27765  clwwlknscsh  27769  erclwwlkntr  27778  eleclclwwlkn  27783  hashecclwwlkn1  27784  umgrhashecclwwlk  27785  clwwlknon0  27800  clwwlknonel  27802  clwwlknon1  27804  clwwlknonwwlknonb  27813  clwwlknonex2lem2  27815  clwwlknun  27819  clwwlkvbij  27820  upgr3v3e3cycl  27887  uhgr3cyclex  27889  upgr4cycl4dv4e  27892  eulerpath  27948  eucrctshift  27950  eucrct2eupth  27952  1to2vfriswmgr  27986  1to3vfriswmgr  27987  3cyclfrgrrn1  27992  4cycl2vnunb  27997  frgrwopreglem2  28020  frgrwopreglem3  28021  frgrwopreglem5ALT  28029  fusgr2wsp2nb  28041  2clwwlk2clwwlklem  28053  2clwwlk2clwwlk  28057  numclwwlk1lem2f1  28064  numclwwlk1lem2fo  28065  numclwwlk1  28068  clwwlknonclwlknonf1o  28069  dlwwlknondlwlknonf1o  28072  numclwlk1  28078  numclwlk2lem2f  28084  numclwlk2lem2f1o  28086  numclwwlk5  28095  frgrreg  28101  frgrregord013  28102  friendship  28106  nsnlplig  28186  nsnlpligALT  28187  isgrpo  28202  vcdi  28270  vcdir  28271  vcass  28272  nmosetre  28469  hlim2  28897  shscli  29022  chintcli  29036  dfch2  29112  spansncvi  29357  nmopsetretALT  29568  nmfnsetre  29582  lnopl  29619  lnfnl  29636  pjss2coi  29869  pjorthcoi  29874  pjscji  29875  pjssdif2i  29879  pjclem4a  29903  pj3lem1  29911  strlem5  29960  hstrlem5  29968  cvmdi  30029  mdslmd3i  30037  atcv1  30085  atcvat4i  30102  cdj3lem2a  30141  cdj3lem3a  30144  opreu2reuALT  30168  iuninc  30241  disji2f  30256  disjif2  30260  fmptcof2  30331  nnindd  30463  xrsmulgzz  30593  ofldchr  30815  esumfzf  31228  issgon  31282  voliune  31388  volfiniune  31389  rrvsum  31612  bnj228  31905  bnj1294  31989  bnj229  32056  bnj607  32088  bnj908  32103  bnj953  32111  bnj1118  32154  bnj1174  32173  bnj1388  32203  funen1cnv  32255  acycgrsubgr  32303  cvmliftlem15  32443  satfsschain  32509  satfdm  32514  satf0op  32522  fmla0xp  32528  gonarlem  32539  goalrlem  32541  satffunlem1lem1  32547  satffunlem2lem1  32549  dmopab3rexdif  32550  satefvfmla0  32563  prv1n  32576  iprodefisumlem  32870  faclimlem1  32873  dfon2lem6  32931  tfisg  32953  poseq  32993  frrlem8  33028  fpr2  33038  frr2  33043  noprefixmo  33100  nosupbnd1lem5  33110  nocvxminlem  33145  nocvxmin  33146  slerec  33175  idinside  33443  onsucconni  33683  axc11n11r  33915  bj-brrelex12ALT  34254  bj-finsumval0  34456  exlimim  34506  exellim  34508  icoreclin  34521  difunieq  34538  fvineqsneq  34576  pibt2  34581  wl-spae  34644  wl-aleq  34657  fin2so  34761  matunitlindf  34772  poimirlem4  34778  poimirlem26  34800  itg2addnclem  34825  upixp  34887  welb  34894  sdclem2  34900  metf1o  34913  sstotbnd3  34937  isbndx  34943  ismtycnv  34963  heiborlem4  34975  bfplem1  34983  opidonOLD  35013  grpomndo  35036  ax12eq  35959  ax12el  35960  cvrat4  36461  mzpexpmpt  39222  diophren  39290  rmxypos  39424  jm2.17a  39437  jm2.17b  39438  rmygeid  39441  jm2.18  39465  jm2.25  39476  jm2.15nn0  39480  jm2.16nn0  39481  pwslnm  39574  isnumbasgrplem1  39581  dgraalem  39625  relexpiidm  39929  relexpmulnn  39934  relexpmulg  39935  relexp01min  39938  relexp0a  39941  relexpxpmin  39942  clsk1indlem3  40273  grucollcld  40476  dvgrat  40524  radcnvrat  40526  sspwimpcf  41134  sspwimpcfVD  41135  e2ebindALT  41143  eu2ndop1stv  43205  afvfv0bi  43232  afveu  43233  afvres  43252  aovmpt4g  43281  ndmaovass  43286  ndmaovdistr  43287  afv2orxorb  43308  afv2eu  43318  imarnf1pr  43362  nltle2tri  43394  fzopredsuc  43404  subsubelfzo0  43407  fzoopth  43408  2ffzoeq  43409  smonoord  43412  iccpartres  43425  iccpartiltu  43429  iccpartigtl  43430  iccpartgt  43434  icceuelpartlem  43442  fargshiftf1  43448  ichnreuop  43481  ichreuopeq  43482  elsprel  43484  sprsymrelfo  43506  prproropf1olem4  43515  paireqne  43520  sbcpr  43530  reupr  43531  goldbachth  43556  fmtnoprmfac1  43574  fmtnoprmfac2  43576  prmdvdsfmtnof1lem2  43594  lighneallem2  43618  lighneallem4  43622  requad2  43635  even3prm2  43731  fpprwpprb  43752  gbegt5  43773  sbgoldbwt  43789  sbgoldbm  43796  nnsum3primesgbe  43804  wtgoldbnnsum4prm  43814  bgoldbnnsum3prm  43816  bgoldbtbndlem2  43818  bgoldbtbndlem3  43819  bgoldbtbndlem4  43820  bgoldbtbnd  43821  isomuspgrlem1  43839  isomuspgrlem2d  43843  upgrwlkupwlk  43862  uspgropssxp  43866  uspgrsprfo  43870  mgmpropd  43889  smndex1mndlem  43979  isassintop  44015  lidldomn1  44090  lidlmmgm  44094  2zlidl  44103  2zrngamgm  44108  2zrngmmgm  44115  rnghmsscmap  44143  rnghmsubcsetclem2  44145  rngcinv  44150  rngccatidALTV  44158  rngcinvALTV  44162  funcrngcsetc  44167  funcrngcsetcALT  44168  rhmsscmap  44189  rhmsubcsetclem2  44191  rhmsubcrngclem2  44197  ringcinv  44201  funcringcsetc  44204  funcringcsetcALTV2lem9  44213  ringccatidALTV  44221  ringcinvALTV  44225  srhmsubc  44245  rhmsubclem4  44258  srhmsubcALTV  44263  rhmsubcALTVlem4  44276  lmodvsmdi  44328  ply1mulgsumlem1  44338  ply1mulgsumlem2  44339  lincdifsn  44377  lincsumcl  44384  lincscmcl  44385  lincext3  44409  lindslinindsimp1  44410  lindslinindsimp2lem5  44415  snlindsntor  44424  lincresunit2  44431  lincresunit3lem2  44433  zgtp1leeq  44474  m1modmmod  44479  elbigo2  44510  fllog2  44526  digexp  44565  dig1  44566  nn0sumshdiglemA  44577  nn0sumshdiglemB  44578  rrxlinec  44621  eenglngeehlnm  44624  rrx2linest  44627  itsclc0yqsol  44649  itsclc0xyqsol  44653
  Copyright terms: Public domain W3C validator