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

Theorem impcom 445
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 444 1 ((𝜓𝜑) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 385
This theorem is referenced by:  mpan9  485  bianir  1029  19.29r  1842  19.41v  1917  19.41vOLD  1970  19.41  2141  nfsb4t  2417  2euex  2573  gencl  3266  2gencl  3267  vtocl4g  3308  rspccva  3339  sseq0  4008  minelOLD  4067  r19.2z  4093  falseral0  4114  elelpwi  4204  eqoreldifOLD  4258  prproe  4466  ssuni  4491  ssuniOLD  4492  disji2  4668  invdisjrab  4671  disjiun  4672  disjxiun  4681  trintss  4802  ssexg  4837  reusv2lem3  4901  propeqop  4999  otiunsndisj  5009  pofun  5080  solin  5087  2optocl  5230  3optocl  5231  ssrelrn  5347  elrnmpt1  5406  resieq  5442  funimaexg  6013  fnun  6035  fss  6094  fun  6104  fvelimab  6292  fvmptss  6331  fvn0ssdmfun  6390  fvcofneq  6407  fmptco  6436  funsndifnop  6456  fnressn  6465  fressnfv  6467  fvn0fvelrn  6470  fmptsng  6475  fvtp2g  6505  fvtp3g  6506  tpres  6507  fnex  6522  funfvima3  6535  isores3  6625  dmfex  7166  el2mpt2csbcl  7295  f1o2ndf1  7330  frxp  7332  fnse  7339  ressuppssdif  7361  funsssuppss  7366  suppss  7370  mpt2xopxnop0  7386  reldmtpos  7405  wfrfun  7470  wfrlem12  7471  smores  7494  tfrlem7  7524  tz7.48-2  7582  tz7.49  7585  oacl  7660  omcl  7661  oecl  7662  oarec  7687  oewordri  7717  oeworde  7718  oelim2  7720  oeoa  7722  oeoelem  7723  oeoe  7724  nnacl  7736  nnmcl  7737  nnecl  7738  nnmsucr  7750  2ecoptocl  7881  undifixp  7986  ssct  8082  xpf1o  8163  limensuc  8178  ac6sfi  8245  frfi  8246  difinf  8271  f1dmvrnfibi  8291  f1vrnfibi  8292  suppeqfsuppbi  8330  elfiun  8377  dffi3  8378  xpwdomg  8531  preleq  8552  infdiffi  8593  epfrs  8645  rankxpsuc  8783  tskwe  8814  infxpenlem  8874  fseqenlem1  8885  kmlem2  9011  cff1  9118  cflim2  9123  sornom  9137  infpssrlem4  9166  fin23lem26  9185  fin23lem30  9202  fin23lem34  9206  isf32lem11  9223  fin67  9255  isfin7-2  9256  fin1a2lem10  9269  axcc2lem  9296  axdc2lem  9308  axdc3lem2  9311  axdc3lem4  9313  axdc4lem  9315  iunfo  9399  tsk0  9623  gruina  9678  grur1a  9679  mulcanenq  9820  reclem2pr  9908  supsrlem  9970  supsr  9971  ax1rid  10020  negf1o  10498  mulgt1  10920  fiminre  11010  lbreu  11011  nnaddcl  11080  nnmulcl  11081  nn0n0n1ge2b  11397  nn0indd  11512  fzind  11513  fnn0ind  11514  uzaddcl  11782  uzinfi  11806  nn01to3  11819  xmulasslem2  12150  supxrunb1  12187  supxrunb2  12188  infmremnf  12211  infmrp1  12212  uzsubsubfz  12401  elfz0ubfz0  12482  fz0fzdiffz0  12487  elfzmlbp  12489  fzofzim  12554  elfzom1elp1fzo  12574  elfzom1p1elfzo  12587  ssfzo12bi  12603  fzonfzoufzol  12611  elfznelfzob  12614  injresinjlem  12628  injresinj  12629  modaddmodup  12773  modfzo0difsn  12782  modsumfzodifsn  12783  addmodlteq  12785  om2uzlti  12789  fsequb  12814  ssnn0fi  12824  ser1const  12897  expcllem  12911  expeq0  12930  faclbnd  13117  faclbnd6  13126  hashf1rn  13181  hashgadd  13204  hashunx  13213  hashnn0n0nn  13218  hashgt0elex  13227  hashss  13235  hashfzp1  13256  hashxp  13259  hashimarni  13266  seqcoll  13286  hash2exprb  13291  hashge2el2difr  13301  elss2prb  13307  brfi1indlem  13316  fi1uzind  13317  brfi1indALT  13320  lswlgt0cl  13389  ccat1st1st  13448  swrdnd  13478  swrd0  13480  swrdsbslen  13494  swrdspsleq  13495  2swrd1eqwrdeq  13500  swrdswrdlem  13505  swrdswrd  13506  wrd2ind  13523  swrdccatfn  13528  swrdccatin1  13529  swrdccatin12lem2a  13531  swrdccatin2  13533  swrdccatin12lem2  13535  swrdccatin12lem3  13536  swrdccatin12  13537  swrdccat3  13538  swrdccat  13539  swrdccat3blem  13541  repswswrd  13577  repswrevw  13579  cshwmodn  13587  cshwsublen  13588  cshwidxmod  13595  cshwidxmodr  13596  cshf1  13602  2cshw  13605  cshweqrep  13613  cshw1  13614  2cshwcshw  13617  cshwcshid  13619  cshwcsh2id  13620  wrdlen2i  13732  2swrd2eqwrdeq  13742  wwlktovfo  13747  relexpsucnnl  13816  rtrclreclem3  13844  rtrclreclem4  13845  relexpindlem  13847  cjexp  13934  absexp  14088  r19.29uz  14134  caubnd  14142  sqreu  14144  climshft  14351  climub  14436  climserle  14437  sumss  14499  sumss2  14501  modfsummods  14569  o1fsum  14589  binom  14606  bcxmas  14611  climcndslem1  14625  climcndslem2  14626  pwm1geoser  14644  cvgrat  14659  clim2prod  14664  prodfn0  14670  prodfrec  14671  ntrivcvgfvn0  14675  fprodn0  14753  fprodmodd  14772  fprodefsum  14869  demoivreALT  14975  znnenlem  14984  ruclem8  15010  dvdsaddre2b  15076  dvdsdivcl  15085  dvdsfac  15095  oddnn02np1  15119  oddge22np1  15120  evennn02n  15121  evennn2n  15122  m1exp1  15140  nn0o  15146  pwp1fsum  15161  flodddiv4  15184  smu01lem  15254  dvdslegcd  15273  gcdneg  15290  dfgcd2  15310  gcdmultiple  15316  seq1st  15331  alginv  15335  lcmf  15393  lcmftp  15396  lcmfunsnlem2lem2  15399  lcmfunsnlem  15401  lcmfun  15405  ncoprmgcdne1b  15410  coprmproddvdslem  15423  coprmproddvds  15424  cncongr1  15428  prmdvdsexp  15474  prmndvdsfaclt  15482  ncoprmlnprm  15483  fvprmselgcd1  15796  prmgaplem6  15807  prmgaplem7  15808  prmgaplem8  15809  cshwshashlem1  15849  setsstruct2  15943  setsstruct  15945  inveq  16481  catsubcat  16546  initoeu2lem0  16710  initoeu2lem1  16711  funcestrcsetclem8  16834  funcestrcsetclem9  16835  fthestrcsetc  16837  fullestrcsetc  16838  funcsetcestrclem9  16850  fthsetcestrc  16852  fullsetcestrc  16853  lubss  17168  lubel  17169  issstrmgm  17299  mgmb1mgm1  17301  frmdgsum  17446  mgm2nsgrplem3  17454  dfgrp2  17494  gaass  17776  gsumwrev  17842  symgextf1lem  17886  symgextf1  17887  fvcosymgeq  17895  gsmsymgreq  17898  symgfixelsi  17901  pmtrprfv3  17920  symggen  17936  pmtrprfval  17953  gsumzres  18356  gsumzunsnd  18401  srgmulgass  18577  srgbinom  18591  lmodvsmmulgdi  18946  lmodfopnelem1  18947  rmodislmodlem  18978  0ringnnzr  19317  assamulgscm  19398  gsumply1subr  19652  gsummoncoe1  19722  pf1ind  19767  cnfldmulg  19826  cnfldexp  19827  psgndiflemB  19994  matmulcell  20299  mat1dimscm  20329  dmatmul  20351  dmatscmcl  20357  scmataddcl  20370  scmatsubcl  20371  scmatsgrp1  20376  mavmulsolcl  20405  ma1repveval  20425  1marepvmarrepid  20429  symgmatr01lem  20507  slesolvec  20533  cramerimplem2  20538  decpmatmullem  20624  pm2mpf1  20652  mp2pm2mplem4  20662  monmat2matmon  20677  chpscmat  20695  chpscmatgsumbin  20697  fvmptnn04ifb  20704  chfacfscmul0  20711  chfacfscmulgsum  20713  chfacfpmmul0  20715  chfacfpmmulgsum  20717  cpmadugsumlemF  20729  clsss  20906  ntrss  20907  restntr  21034  cmpsublem  21250  cmpsub  21251  2ndcrest  21305  txindislem  21484  t0kq  21669  filufint  21771  fbflim2  21828  flftg  21847  alexsubALTlem4  21901  cnextfvval  21916  tmdmulg  21943  ustuqtop4  22095  xmettri2  22192  mettri  22204  metss  22360  tngngp3  22507  clmvscom  22936  lmmbr  23102  caublcls  23153  lmcau  23157  ovolunlem1a  23310  nulmbl2  23350  voliunlem1  23364  iunmbl  23367  volsup  23370  dvlip  23801  dvfsumle  23829  degltlem1  23877  ply1divex  23941  plyco  24042  dgrnznn  24048  dvnply2  24087  plydivex  24097  aannenlem2  24129  aaliou3lem2  24143  ulmcau  24194  zabsle1  25066  gausslemma2dlem1a  25135  gausslemma2dlem2  25137  gausslemma2dlem3  25138  gausslemma2dlem4  25139  2lgslem1a1  25159  dchrisumlem1  25223  dchrisumlem2  25224  dchrisumlem3  25225  qabvle  25359  ostthlem2  25362  ostth2lem2  25368  axeuclidlem  25887  incistruhgr  26019  umgredgprv  26047  umgrpredgv  26080  usgredgprvALT  26132  uhgr2edg  26145  usgredg2vlem2  26163  lfuhgr1v0e  26191  subgrfun  26218  umgrres1lem  26247  upgrres1  26250  fusgrfis  26267  uhgrnbgr0nb  26295  nbgr1vtx  26299  nb3grprlem1  26326  uvtx01vtx  26346  uvtxa01vtx0OLD  26348  fusgrn0degnn0  26451  vtxdginducedm1lem4  26494  finsumvtxdg2size  26502  upgrewlkle2  26558  wlkl1loop  26590  wlkres  26623  lfgrwlknloop  26642  pthdadjvtx  26682  upgr2pthnlp  26684  upgrwlkdvdelem  26688  upgrwlkdvde  26689  uhgrwkspthlem2  26706  usgr2trlspth  26713  usgr2pth  26716  pthdlem2lem  26719  lfgrn1cycl  26753  uspgrn2crct  26756  crctcshwlkn0lem3  26760  crctcshwlkn0lem4  26761  crctcshwlkn0lem5  26762  iswspthsnon  26806  wlkiswwlks1  26821  wlklnwwlkln1  26822  wlkiswwlks2  26829  wlkiswwlksupgr2  26831  wlklnwwlkln2lem  26836  wwlksnred  26855  wwlksnext  26856  wwlksnredwwlkn  26858  wwlksnredwwlkn0  26859  wwlksnextfun  26861  wwlksnextinj  26862  wwlksnextsur  26863  wspthsnonn0vne  26882  wspn0  26889  wwlks2onv  26918  elwwlks2  26933  elwspths2spth  26934  rusgrnumwwlk  26942  clwwlknclwwlkdifsOLD  26947  clwlkclwwlklem2a1  26958  clwlkclwwlklem2fv2  26962  clwlkclwwlklem2a4  26963  clwlkclwwlklem2a  26964  clwlkclwwlklem2  26966  clwwisshclwwslem  26971  clwwisshclwwsn  26973  erclwwlktr  26979  isclwwlknx  26998  clwwlkinwwlk  27003  clwwlkel  27009  clwwlkf  27010  clwwlkf1  27012  clwwlkfo  27013  clwwlkext2edg  27020  wwlksext2clwwlk  27021  wwlksext2clwwlkOLD  27022  wwlksubclwwlk  27023  clwwlknscsh  27027  erclwwlkntr  27035  eleclclwwlkn  27040  hashecclwwlkn1  27041  umgrhashecclwwlk  27042  clwlksfclwwlk  27049  clwlksfoclwwlk  27050  clwwlknon0  27068  clwwlknonel  27070  clwwlknon1  27072  clwwlknonwwlknonb  27080  clwwlknonwwlknonbOLD  27081  clwwlknonex2lem2  27083  clwwlknun  27087  clwwlkvbij  27088  clwwlkvbijOLD  27089  clwwlknunOLD  27091  upgr3v3e3cycl  27158  uhgr3cyclex  27160  upgr4cycl4dv4e  27163  eulerpath  27219  eucrctshift  27221  eucrct2eupth  27223  1to2vfriswmgr  27259  1to3vfriswmgr  27260  3cyclfrgrrn1  27265  4cycl2vnunb  27270  frgrwopreglem2  27293  frgrwopreglem3  27294  frgrwopreglem5ALT  27302  fusgr2wsp2nb  27314  numclwwlk2lem1lemOLD  27325  2clwwlk2clwwlklem1  27327  2clwwlk2clwwlklem2lem2  27329  clwwlkccatlem  27331  2clwwlk2clwwlk  27338  numclwlk1lem2f1  27347  numclwlk1lem2fo  27348  numclwwlk1  27351  numclwlk2lem2f  27357  numclwlk2lem2f1o  27359  numclwlk2lem2fOLD  27364  numclwlk2lem2f1oOLD  27366  numclwwlk5  27375  frgrreg  27381  frgrregord013  27382  friendship  27386  nsnlplig  27463  nsnlpligALT  27464  isgrpo  27479  vcdi  27548  vcdir  27549  vcass  27550  nmosetre  27747  hlim2  28177  shscli  28304  chintcli  28318  dfch2  28394  spansncvi  28639  nmopsetretALT  28850  nmfnsetre  28864  lnopl  28901  lnfnl  28918  pjss2coi  29151  pjorthcoi  29156  pjscji  29157  pjssdif2i  29161  pjclem4a  29185  pj3lem1  29193  strlem5  29242  hstrlem5  29250  cvmdi  29311  mdslmd3i  29319  atcv1  29367  atcvat4i  29384  cdj3lem2a  29423  cdj3lem3a  29426  iuninc  29505  disji2f  29516  disjif2  29520  fmptcof2  29585  nnindd  29694  xrsmulgzz  29806  ofldchr  29942  esumfzf  30259  issgon  30314  voliune  30420  volfiniune  30421  rrvsum  30644  bnj228  30929  bnj1294  31014  bnj229  31080  bnj607  31112  bnj908  31127  bnj953  31135  bnj1118  31178  bnj1174  31197  bnj1388  31227  cvmliftlem15  31406  iprodefisumlem  31752  faclimlem1  31755  dfon2lem6  31817  tfisg  31840  poseq  31878  frrlem5c  31911  noprefixmo  31973  nosupbnd1lem5  31983  nocvxminlem  32018  nocvxmin  32019  slerec  32048  idinside  32316  nn0prpw  32443  onsucconni  32561  axc11n11r  32798  bj-finsumval0  33277  exlimim  33319  exellim  33322  icoreclin  33335  wl-spae  33436  wl-aleq  33452  fin2so  33526  matunitlindf  33537  poimirlem4  33543  poimirlem26  33565  itg2addnclem  33591  upixp  33654  welb  33661  sdclem2  33668  metf1o  33681  sstotbnd3  33705  isbndx  33711  ismtycnv  33731  heiborlem4  33743  bfplem1  33751  opidonOLD  33781  grpomndo  33804  ax12eq  34545  ax12el  34546  cvrat4  35047  mzpexpmpt  37625  diophren  37694  expmordi  37829  rmxypos  37831  jm2.17a  37844  jm2.17b  37845  rmygeid  37848  jm2.18  37872  jm2.25  37883  jm2.15nn0  37887  jm2.16nn0  37888  pwslnm  37981  isnumbasgrplem1  37988  dgraalem  38032  relexpiidm  38313  relexpmulnn  38318  relexpmulg  38319  relexp01min  38322  relexp0a  38325  relexpxpmin  38326  clsk1indlem3  38658  dvgrat  38828  radcnvrat  38830  sspwimpcf  39470  sspwimpcfVD  39471  e2ebindALT  39479  2reurex  41502  2reu1  41507  eu2ndop1stv  41523  afvfv0bi  41553  afveu  41554  afvres  41573  aovmpt4g  41602  ndmaovass  41607  ndmaovdistr  41608  imarnf1pr  41624  nltle2tri  41648  fzopredsuc  41658  subsubelfzo0  41661  fzoopth  41662  2ffzoeq  41663  smonoord  41666  iccpartres  41679  iccpartiltu  41683  iccpartigtl  41684  iccpartgt  41688  icceuelpartlem  41696  fargshiftf1  41702  pfxsuff1eqwrdeq  41732  pfxccatin12lem2  41749  pfxccatin12  41750  pfxccat3  41751  pfxccat3a  41754  cshword2  41762  goldbachth  41784  fmtnoprmfac1  41802  fmtnoprmfac2  41804  prmdvdsfmtnof1lem2  41822  lighneallem2  41848  lighneallem4  41852  even3prm2  41953  gbegt5  41974  sbgoldbwt  41990  sbgoldbm  41997  nnsum3primesgbe  42005  wtgoldbnnsum4prm  42015  bgoldbnnsum3prm  42017  bgoldbtbndlem2  42019  bgoldbtbndlem3  42020  bgoldbtbndlem4  42021  bgoldbtbnd  42022  upgrwlkupwlk  42046  elsprel  42050  sprsymrelfo  42072  uspgropssxp  42077  uspgrsprfo  42081  mgmpropd  42100  isassintop  42171  lidldomn1  42246  lidlmmgm  42250  2zlidl  42259  2zrngamgm  42264  2zrngmmgm  42271  rnghmsscmap  42299  rnghmsubcsetclem2  42301  rngcinv  42306  rngccatidALTV  42314  rngcinvALTV  42318  funcrngcsetc  42323  funcrngcsetcALT  42324  rhmsscmap  42345  rhmsubcsetclem2  42347  rhmsubcrngclem2  42353  ringcinv  42357  funcringcsetc  42360  funcringcsetcALTV2lem9  42369  ringccatidALTV  42377  ringcinvALTV  42381  srhmsubc  42401  rhmsubclem4  42414  srhmsubcALTV  42419  rhmsubcALTVlem4  42432  gsumpr  42464  lmodvsmdi  42488  ply1mulgsumlem1  42499  ply1mulgsumlem2  42500  lincdifsn  42538  lincsumcl  42545  lincscmcl  42546  lincext3  42570  lindslinindsimp1  42571  lindslinindsimp2lem5  42576  snlindsntor  42585  lincresunit2  42592  lincresunit3lem2  42594  lincresunit3  42595  zgtp1leeq  42636  m1modmmod  42641  elbigo2  42671  fllog2  42687  digexp  42726  dig1  42727  nn0sumshdiglemA  42738  nn0sumshdiglemB  42739
  Copyright terms: Public domain W3C validator