MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  com12 Unicode version

Theorem com12 31
Description: Inference that swaps (commutes) antecedents in an implication. Inference associated with pm2.04 82. Its associated inference is mpi 17. (Contributed by NM, 29-Dec-1992.) (Proof shortened by Wolf Lammen, 4-Aug-2012.)
Hypothesis
Ref Expression
com12.1
Assertion
Ref Expression
com12

Proof of Theorem com12
StepHypRef Expression
1 id 22 . 2
2 com12.1 . 2
31, 2syl5com 30 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4
This theorem is referenced by:  syl5  32  syl6com  35  mpcom  36  syli  37  pm2.27  39  pm2.43b  50  syl9r  72  com3r  79  pm2.86i  101  pm2.24  109  con3rr3  136  expt  156  jad  162  pm2.61  171  syl5ibcom  220  syl5ibrcom  222  pm5.501  341  jaod  380  orel1  382  pm2.62  409  impcom  430  impd  431  expcom  435  expd  436  pm3.21  448  simplbi2com  627  imdistanri  691  pm2.64  789  pm2.75  849  ornldOLD  899  ccased  947  dedlem0b  953  3impd  1210  3expd  1213  mp3an1i  1317  ifptru  1388  ifpfal  1389  meredith  1472  19.35  1687  speimfw  1735  sbequ2  1741  equtrr  1797  axc11nlem  1938  cbv1  2017  axc11nlemOLD  2048  dvelimdf  2077  ax12b  2086  equveli  2088  equveliOLD  2089  sbied  2151  sb56  2172  exsb  2212  mo2v  2289  mo2vOLD  2290  mo2vOLDOLD  2291  euex  2308  exmoeu  2316  mo3  2323  mo3OLD  2324  morimvOLD  2342  2mo  2373  2moOLD  2374  2eu1OLD  2377  2eu6  2383  exists2  2389  rexlimdv  2947  r19.12  2983  2gencl  3140  3gencl  3141  rspccv  3207  ceqex  3230  mob  3281  euind  3286  reuind  3303  2rmorex  3304  sseq2  3525  nelss  3562  reupick2  3783  rspn0  3797  uneqdifeq  3916  difsn  4164  eqsn  4191  preq12b  4206  prnebg  4212  iinss2  4382  disjxiun  4449  trint0  4562  dtru  4643  reusv1  4652  reusv2lem1  4653  alxfr  4665  ralxfrALT  4671  sspwb  4701  copsexg  4737  copsexgOLD  4738  pocl  4812  pofun  4821  solin  4828  frss  4851  tz7.7  4909  ordtri3  4919  ordtr2  4927  suc11  4986  onssneli  4992  2optocl  5082  3optocl  5083  ssrel  5096  ssrel2  5098  ssrelrel  5108  relop  5158  restidsing  5335  asymref2  5389  xpidtr  5394  trin2  5395  sotri3  5402  poltletr  5407  xp11  5447  relcnvtr  5532  iotaval  5567  funmo  5609  fss  5744  f0dom0  5774  fv3  5884  tz6.12c  5890  tz6.12i  5891  mpteqb  5970  fveqdmss  6026  eldmrexrnb  6038  funfvima  6147  fvclss  6154  f1veqaeq  6168  isoselem  6237  oprabid  6323  oprabv  6345  ovg  6441  elovmpt2rab  6521  elovmpt2rab1  6522  elovmpt3rab1  6536  sorpsscmpl  6591  iunpw  6614  ordom  6709  limom  6715  peano5  6723  fornex  6769  bropopvvv  6880  f1o2ndf1  6908  poxp  6912  soxp  6913  suppimacnv  6929  ressuppss  6938  ressuppssdif  6940  mpt2xopoveqd  6968  tposfn2  6996  onnseq  7034  smoel  7050  smogt  7057  smoiso2  7059  tfr3  7087  tz7.48-2  7126  tz7.48-3  7128  tz7.49  7129  oecl  7206  oaordex  7226  oalimcl  7228  oaass  7229  omordi  7234  omlimcl  7246  odi  7247  omeulem1  7250  oen0  7254  oewordri  7260  nnawordi  7289  nnaass  7290  nnmordi  7299  omabs  7315  omsmolem  7321  iiner  7402  2ecoptocl  7421  3ecoptocl  7422  undifixp  7525  xpdom2  7632  xpf1o  7699  infensuc  7715  php  7721  onomeneq  7727  isinf  7753  findcard2  7780  unblem2  7793  infssuni  7831  finsschain  7847  fsuppunfi  7869  fsuppunbi  7870  marypha1  7914  hartogs  7990  card2on  8001  card2inf  8002  xpwdomg  8032  elirrv  8044  en3lp  8054  inf3lem1  8066  inf3lem2  8067  inf3lem3  8068  inf3lem5  8070  noinfep  8097  noinfepOLD  8098  trcl  8180  tcel  8197  r1sdom  8213  rankonidlem  8267  scottex  8324  pr2ne  8404  dif1card  8409  fodomnum  8459  cardaleph  8491  kmlem4  8554  kmlem9  8559  kmlem12  8562  kmlem13  8563  cflim2  8664  cfsmolem  8671  infpssrlem3  8706  isfin7-2  8797  fin1a2lem6  8806  fin1a2lem10  8810  fin1a2lem12  8812  domtriomlem  8843  axdc3lem4  8854  axdc4lem  8856  zorn2lem3  8899  zorn2lem4  8900  zorn2lem5  8901  zorn2lem6  8902  zorn2lem7  8903  zornn0g  8906  axdclem  8920  axdclem2  8921  ondomon  8959  alephval2  8968  cfpwsdom  8980  wunr1om  9118  wuncval2  9146  tskr1om  9166  grupr  9196  gruiun  9198  ingru  9214  grothomex  9228  indpi  9306  nqereu  9328  genpnnp  9404  prlem934  9432  ltaddpr2  9434  reclem2pr  9447  mulgt0sr  9503  supsrlem  9509  dedekind  9765  lemul1a  10421  squeeze0  10473  peano5nni  10564  nnunb  10816  nn0lt2  10952  fzind  10987  nn0ind-raph  10989  zindd  10990  eluzadd  11138  uzin  11142  nn01to3  11204  xmulasslem  11506  icoshft  11671  fzen  11732  uzsubsubfz  11736  elfz1b  11777  elfz0ubfz0  11807  elfz0fzfz0  11808  fz0fzelfz0  11809  elfzmlbmOLD  11814  elfzmlbp  11815  elfzodifsumelfzo  11882  ssfzo12bi  11907  elfzonelfzo  11912  elfznelfzo  11915  injresinjlem  11925  injresinj  11926  ssnn0fi  12094  fsuppmapnn0fiub0  12099  expcllem  12177  expeq0  12196  mulexp  12205  leexp2r  12223  bernneq  12292  facdiv  12365  hasheqf1oi  12424  hashf1rn  12425  hashnn0n0nn  12458  hashle00  12465  hashss  12474  hashgt12el  12481  hashgt12el2  12482  hashmap  12493  hashimarni  12497  hash2prde  12516  hash2pwpr  12519  pr2pwpr  12520  hashge2el2dif  12521  hashtpg  12523  hashge3el3dif  12524  hash2sspr  12526  hash1to3  12530  brfi1uzind  12532  ccatsymb  12600  lswccatn0lsw  12607  swrdvalodm2  12664  swrdvalodm  12665  swrdswrdlem  12684  swrdswrd  12685  swrdccatin1  12708  swrdccatin12lem2a  12710  swrdccatin12lem2b  12711  swrdccatin2  12712  swrdccatin12lem2  12714  swrdccatin12lem3  12715  swrdccatin12  12716  swrdccat3  12717  swrdccat  12718  swrdccat3blem  12720  repsdf2  12750  repswswrd  12756  cshwidxmod  12774  cshwidx0  12776  2cshw  12781  cshweqrep  12789  cshw1  12790  cshwsexa  12792  2cshwcshw  12793  scshwfzeqfzo  12794  cshwcshid  12795  cshwcsh2id  12796  swrdco  12803  wwlktovfo  12896  cjexp  12983  absexp  13137  iseraltlem2  13505  modfsummods  13607  clim2prod  13697  prodfn0  13703  prodfrec  13704  prodmo  13743  fprodabs  13778  fprodefsum  13830  sin01gt0  13925  alzdvds  14036  dvdslegcd  14154  gcdneg  14164  rplpwr  14194  qredeq  14247  nnnn0modprm0  14331  prmpwdvds  14422  prmreclem4  14437  ramcl  14547  cshwshashlem1  14580  cshwshashlem2  14581  cshwshashlem3  14582  cshwrepswhash1  14587  imasleval  14938  mreiincl  14993  mreexexd  15045  drsdirfi  15567  isnmgm  15876  sgrpass  15917  mndassOLD  15932  mgm2nsgrplem3  16038  symg2bas  16423  symgfix2  16441  symgextf1  16446  gsmsymgrfix  16453  pmtrprfv3  16479  psgnunilem4  16522  efgi2  16743  lmodvsmmulgdi  17547  0ringnnzr  17917  01eq0ring  17920  mplcoe5lem  18130  mpfrcl  18187  cply1mul  18335  gsummoncoe1  18346  psgndiflemB  18636  psgndiflemA  18637  elfrlmbasn0  18796  lmictra  18880  mamufacex  18891  matecl  18927  dmatelnd  18998  dmatscmcl  19005  scmateALT  19014  scmataddcl  19018  scmatsubcl  19019  scmatsgrp1  19024  scmatf1  19033  mavmulsolcl  19053  gsummatr01lem3  19159  cramerimplem1  19185  cramerimplem2  19186  pmatcollpw3fi1  19289  mp2pm2mplem4  19310  pm2mpfo  19315  chmaidscmat  19349  fvmptnn04ifb  19352  chfacfscmul0  19359  chfacfpmmul0  19363  cayhamlem1  19367  cayhamlem3  19388  cayleyhamilton1  19393  fiinopn  19410  tgcl  19471  distop  19497  isclo2  19589  iscldtop  19596  ssnei2  19617  opnnei  19621  pnfnei  19721  mnfnei  19722  tgcnp  19754  cnpnei  19765  bwthOLD  19911  2ndcctbss  19956  1stcelcls  19962  txcnpi  20109  cnmptcom  20179  fbfinnfr  20342  isfildlem  20358  snfil  20365  fbunfip  20370  fgcl  20379  elfm2  20449  fmfnfmlem1  20455  fmco  20462  fbflim2  20478  flffbas  20496  cnpflf2  20501  flimfcls  20527  tmdgsum  20594  neibl  21004  metcnp3  21043  fgcfil  21710  caubl  21746  volsuplem  21965  ellimc3  22283  dvnadd  22332  dvnres  22334  cpnord  22338  dvnfre  22355  ply1divex  22537  aalioulem2  22729  cxpmul2  23070  wilthlem3  23344  lgsquad2lem2  23634  qabvexp  23811  axcontlem4  24270  uhgraeq12d  24307  ausisusgra  24355  usgraeq12d  24362  usgraedgprv  24376  usgraedgrnv  24377  usgranloop  24379  usgraedg4  24387  usgra1v  24390  usgraidx2v  24393  usgrafisinds  24413  nbgraop  24423  nbusgra  24428  nbgranself2  24436  nbgraf1olem1  24441  nbgraf1olem5  24445  nb3graprlem1  24451  cusgrarn  24459  nbcusgra  24463  cusgrasize2inds  24477  cusgrafi  24482  sizeusglecusglem1  24484  sizeusglecusg  24486  uvtxnbgra  24493  iswlkg  24524  pthdepisspth  24576  spthonepeq  24589  1pthoncl  24594  2pthoncl  24605  redwlk  24608  wlkdvspth  24610  usgra2wlkspthlem1  24619  usgra2wlkspth  24621  cyclnspth  24631  cyclispthon  24633  usgrcyclnl1  24640  nvnencycllem  24643  3v3e3cycl1  24644  constr3trllem2  24651  4cycl4v4e  24666  4cycl4dv  24667  4cycl4dv4e  24668  wwlkn0  24689  wlkiswwlk1  24690  wlkiswwlk2  24697  wlklniswwlkn1  24699  wlklniswwlkn2  24700  usg2wlkeq  24708  wwlknred  24723  wwlknext  24724  wwlknextbi  24725  wwlknredwwlkn  24726  wwlknredwwlkn0  24727  wwlkextwrd  24728  wwlkextinj  24730  wwlkextsur  24731  wwlkextproplem3  24743  wwlkextprop  24744  clwwlkgt0  24771  clwlkisclwwlklem2a4  24784  clwlkisclwwlklem2a  24785  clwlkisclwwlklem1  24787  clwwlkf  24794  clwwlkf1  24796  clwwlkfo  24797  clwwlkvbij  24801  wwlkext2clwwlk  24803  clwwisshclww  24807  erclwwlkeqlen  24812  eleclclwwlknlem2  24818  usg2cwwk2dif  24820  erclwwlkneqlen  24824  eleclclwwlkn  24833  hashecclwwlkn1  24834  usghashecclwwlk  24835  wlklenvclwlk  24839  clwlkfclwwlk  24844  clwlkfoclwwlk  24845  el2wlkonotlem  24862  el2wlkonot  24869  el2spthonot  24870  el2spthonot0  24871  el2wlkonotot0  24872  2wlkonot3v  24875  2spthonot3v  24876  usg2wotspth  24884  2pthwlkonot  24885  2spontn0vne  24887  usg2spthonot  24888  usg2spthonot0  24889  vdusgraval  24907  nbhashuvtx1  24915  rusgrargra  24930  0eusgraiff0rgra  24939  rusgrasn  24945  rusgranumwlk  24957  clwlknclwlkdifs  24960  eupatrl  24968  frgraunss  24995  frgra3vlem1  25000  frgra3vlem2  25001  3vfriswmgralem  25004  3vfriswmgra  25005  2pthfrgra  25011  3cyclfrgrarn1  25012  n4cyclfrgra  25018  frgranbnb  25020  vdn0frgrav2  25023  vdgn0frgrav2  25024  usgn0fidegnn0  25029  frgrancvvdeqlem2  25031  frgrancvvdeqlem3  25032  frgrancvvdeqlem4  25033  frgrancvvdeqlem7  25036  frgrancvvdeqlemA  25037  frgrancvvdeqlemB  25038  frgrancvvdeqlemC  25039  frgrawopreglem3  25046  frgrawopreglem4  25047  frgrawopreglem5  25048  frgrawopreg  25049  frgrawopreg1  25050  frgrawopreg2  25051  frg2wot1  25057  frg2woteqm  25059  frg2woteq  25060  2spotdisj  25061  usg2spot2nb  25065  usgreg2spot  25067  2spotmdisj  25068  frgregordn0  25070  extwwlkfablem2  25078  numclwwlkun  25079  numclwwlkovf2ex  25086  numclwwlkovgelim  25089  extwwlkfab  25090  numclwlk1lem2foa  25091  numclwlk1lem2f1  25094  numclwlk1lem2fo  25095  numclwwlk1  25098  numclwwlk2lem1  25102  numclwlk2lem2f  25103  numclwlk2lem2f1o  25105  frgrareggt1  25116  frgrareg  25117  frgraregord013  25118  frgraregord13  25119  friendshipgt3  25121  friendship  25122  gxnn0add  25276  gxnn0mul  25279  ismgmOLD  25322  isexid2  25327  zerdivemp1  25436  ipassi  25756  ubthlem2  25787  isch3  26159  shintcli  26247  shmodsi  26307  spansncvi  26570  pjjsi  26618  hoaddsub  26735  eigorthi  26756  pjss2coi  27083  pjnormssi  27087  pj3cor1i  27128  strb  27177  dmdmd  27219  mdsl0  27229  csmdsymi  27253  chrelat2i  27284  cvati  27285  mdsymlem3  27324  mdsymlem6  27327  sumdmdlem2  27338  dmdbr5ati  27341  ssrelf  27466  cvmlift2lem1  28747  mrsubvrs  28882  mclsax  28929  3ccased  29096  binomfallfac  29163  dfres3  29188  dfon2lem3  29217  rdgprc  29227  trpredmintr  29314  trpredrec  29321  wfr3g  29342  wfrlem12  29354  frr3g  29386  frrlem11  29399  sltval2  29416  cgrextend  29658  btwndiff  29677  btwnconn1lem12  29748  brsegle  29758  broutsideof2  29772  funray  29790  meran1  29876  waj-ax  29879  arg-ax  29881  wl-dral1d  29984  wl-exeq  29987  wl-lem-exsb  30015  elicc3  30135  nn0prpwlem  30140  nn0prpw  30141  fnessref  30175  neibastop2lem  30178  filnetlem4  30199  fzmul  30233  fdc  30238  seqpo  30240  incsequz  30241  isismty  30297  ismtybndlem  30302  heibor1lem  30305  ghomco  30345  zerdivemp1x  30358  pridlc  30468  ceqsex3OLD  30601  incssnn0  30643  fphpd  30750  jm2.19lem3  30933  setindtr  30966  dfac21  31012  islssfg2  31017  mpaaeu  31099  nzss  31222  stoweidlem26  31808  hirstL-ax3  32087  rexsb  32173  rexrsb  32174  2reu1  32191  afvres  32257  tz6.12-afv  32258  afvco2  32261  ndmaovdistr  32292  zm1nn  32325  ssfz12  32330  fzoopth  32340  2ffzoeq  32341  lswn0  32343  usgra2pthspth  32351  usgra2pthlem1  32353  usgra2pth  32354  uhgrauhgbi  32374  usgedgvadf1  32415  usgedgvadf1ALT  32418  mgmhmlin  32474  issubmgm2  32478  tpres  32554  inveq  32565  cicsym  32588  cictr  32589  initoid  32611  termoid  32612  initoeu1  32617  initoeu2lem0  32619  initoeu2lem1  32620  initoeu2lem2  32621  initoeu2  32622  termoeu1  32624  fthestrcsetc  32656  fthsetcestrc  32671  lmod0rng  32674  lidldomn1  32727  lidlmmgm  32731  rnghmsscmap  32782  rnghmsubcsetclem2  32784  rngcinv  32789  rngccatidOLD  32797  rngcinvOLD  32801  funcrngcsetc  32806  funcrngcsetcALT  32807  rhmsscmap  32828  rhmsubcsetclem2  32830  rhmsubcrngclem2  32836  ringcinv  32840  ringcbasbas  32842  funcringcsetc  32843  funcringcsetcOLD2lem9  32852  ringccatidOLD  32860  ringcinvOLD  32864  ringcbasbasOLD  32866  rhmsubclem4  32897  rhmsubcOLDlem4  32916  ztprmneprm  32936  nn0le2is012  32956  pgrpgt2nabl  32959  lmodvsmdi  32975  ply1mulgsumlem2  32987  lincsumcl  33032  ellcoellss  33036  linindslinci  33049  islinindfis  33050  lincext3  33057  lindslinindsimp1  33058  lindslinindimp2lem4  33062  lindslinindsimp2lem5  33063  lindslinindsimp2  33064  lindsrng01  33069  ldepspr  33074  lincresunit3lem1  33080  ldepsnlinclem1  33106  ldepsnlinclem2  33107  sb5ALT  33295  truniALT  33312  ee223  33420  3orbi123VD  33650  sbc3orgVD  33651  exbirVD  33653  exbiriVD  33654  sbcim2gVD  33675  trsbcVD  33677  truniALTVD  33678  onfrALTlem3VD  33687  onfrALTlem2VD  33689  csbrngVD  33696  19.41rgVD  33702  ax6e2eqVD  33707  ax6e2ndeqVD  33709  2uasbanhVD  33711  sb5ALTVD  33713  vk15.4jVD  33714  bj-con2com  34139  bj-axdd2  34180  bj-cbv1v  34292  bj-axc11nlemv  34315  bj-sb56  34349  bj-dtru  34383  bj-snsetex  34521  bj-finsumval0  34663  cdleme18d  36020  tendovalco  36491  cdlemn11pre  36937  dihord2pre  36952  psshepw  37811  syldbl2  37985
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator