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

Theorem impcom 446
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 445 1 ((𝜓𝜑) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 197  df-an 386
This theorem is referenced by:  mpan9  486  bianir  1008  19.29r  1800  19.41v  1912  equtr2OLD  1954  equvinvOLD  1960  19.41  2101  nfsb4t  2387  2euex  2542  gencl  3230  2gencl  3231  vtocl4g  3272  rspccva  3303  sseq0  3966  minelOLD  4025  r19.2z  4051  falseral0  4072  elelpwi  4162  eqoreldifOLD  4217  prproe  4425  ssuni  4450  ssuniOLD  4451  disji2  4627  invdisjrab  4630  disjiun  4631  disjxiun  4640  trintss  4760  ssexg  4795  reusv2lem3  4862  propeqop  4960  otiunsndisj  4970  pofun  5041  solin  5048  2optocl  5186  3optocl  5187  ssrelrn  5304  elrnmpt1  5363  resieq  5395  funimaexg  5963  fnun  5985  fss  6043  fun  6053  fvelimab  6240  fvmptss  6279  fvn0ssdmfun  6336  fvcofneq  6353  fmptco  6382  funsndifnop  6401  fnressn  6410  fressnfv  6412  fvn0fvelrn  6415  fmptsng  6419  fvtp2g  6449  fvtp3g  6450  tpres  6451  fnex  6466  funfvima3  6480  isores3  6570  dmfex  7109  el2mpt2csbcl  7235  f1o2ndf1  7270  frxp  7272  fnse  7279  ressuppssdif  7301  funsssuppss  7306  suppss  7310  mpt2xopxnop0  7326  reldmtpos  7345  wfrfun  7410  wfrlem12  7411  smores  7434  tfrlem7  7464  tz7.48-2  7522  tz7.49  7525  oacl  7600  omcl  7601  oecl  7602  oarec  7627  oewordri  7657  oeworde  7658  oelim2  7660  oeoa  7662  oeoelem  7663  oeoe  7664  nnacl  7676  nnmcl  7677  nnecl  7678  nnmsucr  7690  2ecoptocl  7823  undifixp  7929  ssct  8026  xpf1o  8107  limensuc  8122  ac6sfi  8189  frfi  8190  difinf  8215  f1dmvrnfibi  8235  f1vrnfibi  8236  suppeqfsuppbi  8274  elfiun  8321  dffi3  8322  xpwdomg  8475  preleq  8499  infdiffi  8540  epfrs  8592  rankxpsuc  8730  tskwe  8761  infxpenlem  8821  fseqenlem1  8832  kmlem2  8958  cff1  9065  cflim2  9070  sornom  9084  infpssrlem4  9113  fin23lem26  9132  fin23lem30  9149  fin23lem34  9153  isf32lem11  9170  fin67  9202  isfin7-2  9203  fin1a2lem10  9216  axcc2lem  9243  axdc2lem  9255  axdc3lem2  9258  axdc3lem4  9260  axdc4lem  9262  iunfo  9346  tsk0  9570  gruina  9625  grur1a  9626  mulcanenq  9767  reclem2pr  9855  supsrlem  9917  supsr  9918  ax1rid  9967  negf1o  10445  mulgt1  10867  fiminre  10957  lbreu  10958  nnaddcl  11027  nnmulcl  11028  nn0n0n1ge2b  11344  nn0indd  11459  fzind  11460  fnn0ind  11461  uzaddcl  11729  uzinfi  11753  nn01to3  11766  xmulasslem2  12097  supxrunb1  12134  supxrunb2  12135  infmremnf  12158  infmrp1  12159  uzsubsubfz  12348  elfz1b  12394  elfz0ubfz0  12427  fz0fzdiffz0  12432  elfzmlbp  12434  fzofzim  12498  elfzom1elp1fzo  12518  elfzom1p1elfzo  12531  ssfzo12bi  12547  fzonfzoufzol  12555  elfznelfzob  12558  injresinjlem  12571  injresinj  12572  modaddmodup  12716  modfzo0difsn  12725  modsumfzodifsn  12726  addmodlteq  12728  om2uzlti  12732  fsequb  12757  ssnn0fi  12767  ser1const  12840  expcllem  12854  expeq0  12873  faclbnd  13060  faclbnd6  13069  hasheqf1oiOLD  13124  hashf1rn  13125  hashf1rnOLD  13126  hashgadd  13149  hashunx  13158  hashnn0n0nn  13163  hashgt0elex  13172  hashss  13180  hashfzp1  13201  hashxp  13204  hashimarni  13211  seqcoll  13231  hash2exprb  13236  hashge2el2difr  13246  elss2prb  13252  brfi1indlem  13261  fi1uzind  13262  brfi1indALT  13265  fi1uzindOLD  13268  brfi1indALTOLD  13271  lswlgt0cl  13339  swrdnd  13414  swrd0  13416  swrdsbslen  13430  swrdspsleq  13431  2swrd1eqwrdeq  13436  swrdswrdlem  13441  swrdswrd  13442  wrd2ind  13459  swrdccatfn  13463  swrdccatin1  13464  swrdccatin12lem2a  13466  swrdccatin2  13468  swrdccatin12lem2  13470  swrdccatin12lem3  13471  swrdccatin12  13472  swrdccat3  13473  swrdccat  13474  swrdccat3blem  13476  repswswrd  13512  repswrevw  13514  cshwmodn  13522  cshwsublen  13523  cshwidxmod  13530  cshwidxmodr  13531  cshf1  13537  2cshw  13540  cshweqrep  13548  cshw1  13549  2cshwcshw  13552  cshwcshid  13554  cshwcsh2id  13555  wrdlen2i  13667  2swrd2eqwrdeq  13677  wwlktovfo  13682  relexpsucnnl  13753  rtrclreclem3  13781  rtrclreclem4  13782  relexpindlem  13784  cjexp  13871  absexp  14025  r19.29uz  14071  caubnd  14079  sqreu  14081  climshft  14288  climub  14373  climserle  14374  sumss  14436  sumss2  14438  modfsummods  14506  o1fsum  14526  binom  14543  bcxmas  14548  climcndslem1  14562  climcndslem2  14563  pwm1geoser  14581  cvgrat  14596  clim2prod  14601  prodfn0  14607  prodfrec  14608  ntrivcvgfvn0  14612  fprodn0  14690  fprodmodd  14709  fprodefsum  14806  demoivreALT  14912  znnenlem  14921  ruclem8  14947  dvdsaddre2b  15010  dvdsdivcl  15019  dvdsfac  15029  oddnn02np1  15053  oddge22np1  15054  evennn02n  15055  evennn2n  15056  m1exp1  15074  nn0o  15080  pwp1fsum  15095  flodddiv4  15118  smu01lem  15188  dvdslegcd  15207  gcdneg  15224  dfgcd2  15244  gcdmultiple  15250  seq1st  15265  alginv  15269  lcmf  15327  lcmftp  15330  lcmfunsnlem2lem2  15333  lcmfunsnlem  15335  lcmfun  15339  ncoprmgcdne1b  15344  coprmproddvdslem  15357  coprmproddvds  15358  cncongr1  15362  prmdvdsexp  15408  prmndvdsfaclt  15416  ncoprmlnprm  15417  fvprmselgcd1  15730  prmgaplem6  15741  prmgaplem7  15742  prmgaplem8  15743  cshwshashlem1  15783  setsstruct2  15877  setsstruct  15879  inveq  16415  catsubcat  16480  initoeu2lem0  16644  initoeu2lem1  16645  funcestrcsetclem8  16768  funcestrcsetclem9  16769  fthestrcsetc  16771  fullestrcsetc  16772  funcsetcestrclem9  16784  fthsetcestrc  16786  fullsetcestrc  16787  lubss  17102  lubel  17103  issstrmgm  17233  mgmb1mgm1  17235  frmdgsum  17380  mgm2nsgrplem3  17388  dfgrp2  17428  gaass  17711  gsumwrev  17777  symgextf1lem  17821  symgextf1  17822  fvcosymgeq  17830  gsmsymgreq  17833  symgfixelsi  17836  pmtrprfv3  17855  symggen  17871  pmtrprfval  17888  gsumzres  18291  gsumzunsnd  18336  srgmulgass  18512  srgbinom  18526  lmodvsmmulgdi  18879  lmodfopnelem1  18880  rmodislmodlem  18911  0ringnnzr  19250  assamulgscm  19331  gsumply1subr  19585  gsummoncoe1  19655  pf1ind  19700  cnfldmulg  19759  cnfldexp  19760  psgndiflemB  19927  matmulcell  20232  mat1dimscm  20262  dmatmul  20284  dmatscmcl  20290  scmataddcl  20303  scmatsubcl  20304  scmatsgrp1  20309  mavmulsolcl  20338  ma1repveval  20358  1marepvmarrepid  20362  symgmatr01lem  20440  slesolvec  20466  cramerimplem2  20471  decpmatmullem  20557  pm2mpf1  20585  mp2pm2mplem4  20595  monmat2matmon  20610  chpscmat  20628  chpscmatgsumbin  20630  fvmptnn04ifb  20637  chfacfscmul0  20644  chfacfscmulgsum  20646  chfacfpmmul0  20648  chfacfpmmulgsum  20650  cpmadugsumlemF  20662  clsss  20839  ntrss  20840  restntr  20967  cmpsublem  21183  cmpsub  21184  2ndcrest  21238  txindislem  21417  t0kq  21602  filufint  21705  fbflim2  21762  flftg  21781  alexsubALTlem4  21835  cnextfvval  21850  tmdmulg  21877  ustuqtop4  22029  xmettri2  22126  mettri  22138  metss  22294  tngngp3  22441  clmvscom  22871  lmmbr  23037  caublcls  23088  lmcau  23092  ovolunlem1a  23245  nulmbl2  23285  voliunlem1  23299  iunmbl  23302  volsup  23305  dvlip  23737  dvfsumle  23765  degltlem1  23813  ply1divex  23877  plyco  23978  dgrnznn  23984  dvnply2  24023  plydivex  24033  aannenlem2  24065  aaliou3lem2  24079  ulmcau  24130  zabsle1  25002  gausslemma2dlem1a  25071  gausslemma2dlem2  25073  gausslemma2dlem3  25074  gausslemma2dlem4  25075  2lgslem1a1  25095  dchrisumlem1  25159  dchrisumlem2  25160  dchrisumlem3  25161  qabvle  25295  ostthlem2  25298  ostth2lem2  25304  axeuclidlem  25823  incistruhgr  25955  umgredgprv  25983  umgrpredgv  26016  usgredgprvALT  26068  uhgr2edg  26081  usgredg2vlem2  26099  lfuhgr1v0e  26127  subgrfun  26154  umgrres1lem  26183  upgrres1  26186  fusgrfis  26203  uhgrnbgr0nb  26231  nbgr1vtx  26235  nb3grprlem1  26263  uvtxa01vtx0  26278  uvtx2vtx1edg  26280  fusgrn0degnn0  26376  vtxdginducedm1lem4  26419  finsumvtxdg2size  26427  upgrewlkle2  26483  wlkl1loop  26515  wlkres  26548  lfgrwlknloop  26567  pthdadjvtx  26607  upgr2pthnlp  26609  upgrwlkdvdelem  26613  upgrwlkdvde  26614  uhgrwkspthlem2  26631  usgr2trlspth  26638  usgr2pth  26641  pthdlem2lem  26644  lfgrn1cycl  26678  uspgrn2crct  26681  crctcshwlkn0lem3  26685  crctcshwlkn0lem4  26686  crctcshwlkn0lem5  26687  wspthnonp  26725  wlkiswwlks1  26734  wlklnwwlkln1  26735  wlkiswwlks2  26742  wlkiswwlksupgr2  26744  wlklnwwlkln2lem  26749  wwlksnred  26768  wwlksnext  26769  wwlksnredwwlkn  26771  wwlksnredwwlkn0  26772  wwlksnextfun  26774  wwlksnextinj  26775  wwlksnextsur  26776  wspthsnonn0vne  26794  wspn0  26801  wwlks2onv  26828  elwwlks2  26842  elwspths2spth  26843  rusgrnumwwlk  26851  clwwlknclwwlkdifs  26854  isclwwlksnx  26870  clwlkclwwlklem2a1  26874  clwlkclwwlklem2fv2  26878  clwlkclwwlklem2a4  26879  clwlkclwwlklem2a  26880  clwlkclwwlklem2  26882  clwwlksel  26894  clwwlksf  26895  clwwlksf1  26897  clwwlksfo  26898  clwwlksnwwlkncl  26901  clwwlksvbij  26902  clwwlksext2edg  26903  wwlksext2clwwlk  26904  wwlksubclwwlks  26905  clwwisshclwwslem  26907  clwwisshclwwsn  26909  erclwwlkstr  26916  clwwlksnscsh  26920  erclwwlksntr  26928  eleclclwwlksn  26933  hashecclwwlksn1  26934  umgrhashecclwwlk  26935  clwlksfclwwlk  26942  clwlksfoclwwlk  26943  clwwlksnun  26954  upgr3v3e3cycl  27020  uhgr3cyclex  27022  upgr4cycl4dv4e  27025  eulerpath  27081  eucrctshift  27083  eucrct2eupth  27085  1to2vfriswmgr  27123  1to3vfriswmgr  27124  3cyclfrgrrn1  27129  4cycl2vnunb  27134  frgrwopreglem2  27155  frgrwopreglem3  27156  fusgr2wsp2nb  27172  clwwlkextfrlem1  27183  numclwwlkovf2ex  27191  numclwlk1lem2foa  27195  numclwlk1lem2f1  27198  numclwlk1lem2fo  27199  numclwwlk1  27202  numclwlk2lem2f  27207  numclwlk2lem2f1o  27209  numclwwlk5  27216  frgrreg  27222  frgrregord013  27223  friendship  27227  nsnlplig  27303  nsnlpligALT  27304  isgrpo  27321  vcdi  27390  vcdir  27391  vcass  27392  nmosetre  27589  hlim2  28019  shscli  28146  chintcli  28160  dfch2  28236  spansncvi  28481  nmopsetretALT  28692  nmfnsetre  28706  lnopl  28743  lnfnl  28760  pjss2coi  28993  pjorthcoi  28998  pjscji  28999  pjssdif2i  29003  pjclem4a  29027  pj3lem1  29035  strlem5  29084  hstrlem5  29092  cvmdi  29153  mdslmd3i  29161  atcv1  29209  atcvat4i  29226  cdj3lem2a  29265  cdj3lem3a  29268  iuninc  29351  disji2f  29362  disjif2  29366  fmptcof2  29430  nnindd  29540  xrsmulgzz  29652  ofldchr  29788  esumfzf  30105  issgon  30160  voliune  30266  volfiniune  30267  rrvsum  30490  bnj228  30777  bnj1294  30862  bnj229  30928  bnj607  30960  bnj908  30975  bnj953  30983  bnj1118  31026  bnj1174  31045  bnj1388  31075  cvmliftlem15  31254  iprodefisumlem  31601  faclimlem1  31604  dfon2lem6  31667  tfisg  31690  poseq  31724  frrlem4  31757  frrlem5c  31760  frrlem11  31766  noprefixmo  31822  nosupbnd1lem5  31832  nocvxminlem  31867  nocvxmin  31868  slerec  31897  idinside  32166  nn0prpw  32293  onsucconni  32411  axc11n11r  32648  bj-finsumval0  33118  exlimim  33160  exellim  33163  icoreclin  33176  wl-spae  33277  wl-aleq  33293  fin2so  33367  matunitlindf  33378  poimirlem4  33384  poimirlem26  33406  itg2addnclem  33432  upixp  33495  welb  33502  sdclem2  33509  metf1o  33522  sstotbnd3  33546  isbndx  33552  ismtycnv  33572  heiborlem4  33584  bfplem1  33592  opidonOLD  33622  grpomndo  33645  ax12eq  34045  ax12el  34046  cvrat4  34548  mzpexpmpt  37127  diophren  37196  expmordi  37331  rmxypos  37333  jm2.17a  37346  jm2.17b  37347  rmygeid  37350  jm2.18  37374  jm2.25  37385  jm2.15nn0  37389  jm2.16nn0  37390  pwslnm  37483  isnumbasgrplem1  37490  dgraalem  37534  relexpiidm  37815  relexpmulnn  37820  relexpmulg  37821  relexp01min  37824  relexp0a  37827  relexpxpmin  37828  clsk1indlem3  38161  dvgrat  38331  radcnvrat  38333  sspwimpcf  38976  sspwimpcfVD  38977  e2ebindALT  38985  2reurex  40944  2reu1  40949  eu2ndop1stv  40965  afvfv0bi  40995  afveu  40996  afvres  41015  aovmpt4g  41044  ndmaovass  41049  ndmaovdistr  41050  imarnf1pr  41064  nltle2tri  41086  fzopredsuc  41096  subsubelfzo0  41099  fzoopth  41100  2ffzoeq  41101  smonoord  41105  iccpartres  41118  iccpartiltu  41122  iccpartigtl  41123  iccpartgt  41127  icceuelpartlem  41135  fargshiftf1  41141  pfxsuff1eqwrdeq  41172  pfxccatin12lem2  41189  pfxccatin12  41190  pfxccat3  41191  pfxccat3a  41194  cshword2  41202  goldbachth  41224  fmtnoprmfac1  41242  fmtnoprmfac2  41244  prmdvdsfmtnof1lem2  41262  lighneallem2  41288  lighneallem4  41292  even3prm2  41393  gbegt5  41414  sbgoldbwt  41430  sbgoldbm  41437  nnsum3primesgbe  41445  wtgoldbnnsum4prm  41455  bgoldbnnsum3prm  41457  bgoldbtbndlem2  41459  bgoldbtbndlem3  41460  bgoldbtbndlem4  41461  bgoldbtbnd  41462  upgrwlkupwlk  41486  elsprel  41490  sprsymrelfo  41512  uspgropssxp  41517  uspgrsprfo  41521  mgmpropd  41540  isassintop  41611  lidldomn1  41686  lidlmmgm  41690  2zlidl  41699  2zrngamgm  41704  2zrngmmgm  41711  rnghmsscmap  41739  rnghmsubcsetclem2  41741  rngcinv  41746  rngccatidALTV  41754  rngcinvALTV  41758  funcrngcsetc  41763  funcrngcsetcALT  41764  rhmsscmap  41785  rhmsubcsetclem2  41787  rhmsubcrngclem2  41793  ringcinv  41797  funcringcsetc  41800  funcringcsetcALTV2lem9  41809  ringccatidALTV  41817  ringcinvALTV  41821  srhmsubc  41841  rhmsubclem4  41854  srhmsubcALTV  41859  rhmsubcALTVlem4  41872  gsumpr  41904  lmodvsmdi  41928  ply1mulgsumlem1  41939  ply1mulgsumlem2  41940  lincdifsn  41978  lincsumcl  41985  lincscmcl  41986  lincext3  42010  lindslinindsimp1  42011  lindslinindsimp2lem5  42016  snlindsntor  42025  lincresunit2  42032  lincresunit3lem2  42034  lincresunit3  42035  zgtp1leeq  42076  m1modmmod  42081  elbigo2  42111  fllog2  42127  digexp  42166  dig1  42167  nn0sumshdiglemA  42178  nn0sumshdiglemB  42179
  Copyright terms: Public domain W3C validator