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

Theorem com12 32
Description: Inference that swaps (commutes) antecedents in an implication. Inference associated with pm2.04 90. Its associated inference is mpi 20. (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 31 1 (𝜓 → (𝜑𝜒))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  syl11  33  syl5  34  syl6com  37  mpcom  38  syli  39  syl2imc  41  pm2.27  42  syldc  48  pm2.43b  55  syl9r  78  com3r  87  pm2.24  121  con3rr3  151  expt  168  jad  174  pm2.61  183  syl5ibcom  235  syl5ibrcom  237  pm5.501  355  jaod  394  orel1  396  pm2.62  424  impcom  445  impd  446  expcom  450  expd  451  pm3.21  463  simplbi2com  656  imdistanri  727  pm2.64  847  pm2.75  912  ccased  1007  dedlem0b  1013  3impd  1303  3expd  1306  mp3an1i  1457  minimp  1600  meredith  1606  19.35  1845  speimfw  1933  sbequ2  1939  equtrr  1995  equeucl  1997  sb56  2188  cbv1  2303  axc11n  2342  dvelimdf  2366  ax12b  2373  equvel  2375  sbied  2437  exsb  2496  mo2v  2505  euex  2522  exmoeu  2531  mo3  2536  2mo  2580  2eu6  2587  exists2  2591  rexlimdv  3059  r19.12  3092  2gencl  3267  3gencl  3268  rspccv  3337  ceqex  3364  mob  3421  euind  3426  reuind  3444  sseq2  3660  nelss  3697  reupick2  3946  rspn0  3967  uneqdifeq  4090  uneqdifeqOLD  4091  eqoreldifOLD  4258  ssprsseq  4389  eqsnOLD  4394  preq12b  4413  prel12  4414  prnebg  4420  3elpr2eq  4467  iinss2  4604  disjxiunOLD  4682  trintss  4802  dtru  4887  reusv1OLD  4897  reusv2lem1  4898  alxfr  4908  ralxfrALT  4917  sspwb  4947  copsexg  4985  propeqop  4999  pocl  5071  pofun  5080  solin  5087  frss  5110  2optocl  5230  3optocl  5231  ssrel  5241  ssrelOLD  5242  ssrel2  5244  ssrelrel  5254  relop  5305  dfres3  5433  restidsingOLD  5494  asymref2  5548  xpidtr  5553  trin2  5554  poltletr  5563  xp11  5604  relcnvtr  5693  tz7.7  5787  ordtri3OLD  5798  ordtr2  5806  suc11  5869  iotaval  5900  funmo  5942  fundif  5973  fss  6094  f0dom0  6127  fv3  6244  tz6.12c  6251  tz6.12i  6252  mpteqb  6338  fveqdmss  6394  eldmrexrnb  6406  funopsn  6453  funsndifnop  6456  tpres  6507  funfvima  6532  fvclss  6540  f1veqaeq  6554  isoselem  6631  oprabv  6745  ovg  6841  elovmpt3rab1  6935  sorpsscmpl  6990  iunpw  7020  ordom  7116  limom  7122  peano5  7131  fornex  7177  bropopvvv  7300  bropfvvvvlem  7301  f1o2ndf1  7330  poxp  7334  soxp  7335  suppimacnv  7351  ressuppss  7359  ressuppssdif  7361  tposfn2  7419  wfr3g  7458  onnseq  7486  smoel  7502  smogt  7509  smoiso2  7511  tfr3  7540  tz7.48-2  7582  tz7.48-3  7584  tz7.49  7585  oecl  7662  oaordex  7683  oalimcl  7685  oaass  7686  omordi  7691  omlimcl  7703  odi  7704  omeulem1  7707  oen0  7711  nnawordi  7746  nnaass  7747  nnmordi  7756  omabs  7772  omsmolem  7778  iiner  7862  2ecoptocl  7881  3ecoptocl  7882  undifixp  7986  xpdom2  8096  xpf1o  8163  infensuc  8179  php  8185  onomeneq  8191  isinf  8214  findcard2  8241  unblem2  8254  infssuni  8298  finsschain  8314  fsuppunfi  8336  fsuppunbi  8337  marypha1  8381  hartogs  8490  card2on  8500  card2inf  8501  xpwdomg  8531  elirrv  8542  en3lp  8551  inf3lem1  8563  inf3lem2  8564  inf3lem3  8565  inf3lem5  8567  noinfep  8595  trcl  8642  tcel  8659  rankonidlem  8729  scottex  8786  dif1card  8871  fodomnum  8918  cardaleph  8950  kmlem9  9018  kmlem13  9022  cflim2  9123  cfsmolem  9130  infpssrlem3  9165  isfin7-2  9256  fin1a2lem6  9265  fin1a2lem10  9269  fin1a2lem12  9271  domtriomlem  9302  axdc3lem4  9313  axdc4lem  9315  zorn2lem3  9358  zorn2lem4  9359  zorn2lem5  9360  zorn2lem7  9362  zornn0g  9365  axdclem2  9380  ondomon  9423  alephval2  9432  cfpwsdom  9444  wuncval2  9607  grupr  9657  gruiun  9659  ingru  9675  grothomex  9689  indpi  9767  nqereu  9789  prlem934  9893  reclem2pr  9908  mulgt0sr  9964  supsrlem  9970  dedekind  10238  lemul1a  10915  squeeze0  10964  peano5nni  11061  nnunb  11326  nn0lt2  11478  nn0le2is012  11479  fzind  11513  nn0ind-raph  11515  zindd  11516  eluzadd  11754  uzin  11758  nn01to3  11819  xnn0xadd0  12115  xmulasslem  12153  icoshft  12332  fzen  12396  uzsubsubfz  12401  elfz0ubfz0  12482  elfz0fzfz0  12483  fz0fzelfz0  12484  elfzmlbp  12489  elfzodifsumelfzo  12573  ssfzo12bi  12603  elfzonelfzo  12610  elfznelfzo  12613  injresinjlem  12628  injresinj  12629  modfzo0difsn  12782  modsumfzodifsn  12783  addmodlteq  12785  ssnn0fi  12824  fsuppmapnn0fiub0  12833  expcllem  12911  expeq0  12930  mulexp  12939  leexp2r  12958  bernneq  13030  facdiv  13114  hasheqf1oi  13180  hashnn0n0nn  13218  hashss  13235  hashgt12el  13248  hashgt12el2  13249  hashmap  13260  hashimarni  13266  hash2prde  13290  hashle2pr  13297  pr2pwpr  13299  hashge2el2dif  13300  hashge2el2difr  13301  hashtpg  13305  hashge3el3dif  13306  exprelprel  13309  hash1to3  13311  fundmge2nop0  13312  fi1uzind  13317  ccatsymb  13400  swrdnd  13478  swrdnd2  13479  swrdswrdlem  13505  swrdswrd  13506  swrdccatin1  13529  swrdccatin12lem2a  13531  swrdccatin12lem2b  13532  swrdccatin2  13533  swrdccatin12lem2  13535  swrdccatin12lem3  13536  swrdccat3  13538  swrdccat  13539  swrdccat3blem  13541  repsdf2  13571  repswswrd  13577  cshwidxmod  13595  cshwidx0  13598  cshf1  13602  2cshw  13605  cshweqrep  13613  cshw1  13614  cshwsexa  13616  2cshwcshw  13617  scshwfzeqfzo  13618  cshwcsh2id  13620  swrdco  13629  wwlktovfo  13747  relexpaddg  13837  cjexp  13934  absexp  14088  iseraltlem2  14457  modfsummods  14569  clim2prod  14664  prodfn0  14670  prodfrec  14671  prodmo  14710  fprodabs  14748  binomfallfac  14816  fprodefsum  14869  dvdsaddre2b  15076  addmodlteqALT  15094  oddge22np1  15120  nn0enne  15141  nn0o1gt2  15144  sumeven  15157  sumodd  15158  dvdslegcd  15273  gcdneg  15290  dfgcd2  15310  rplpwr  15323  lcmf  15393  lcmftp  15396  lcmfunsnlem2lem1  15398  lcmfunsnlem2  15400  lcmfdvds  15402  lcmfdvdsb  15403  lcmfunsn  15404  coprmdvds1  15412  qredeq  15418  coprmprod  15422  coprmproddvdslem  15423  cncongr1  15428  cncongr2  15429  prm2orodd  15451  nnnn0modprm0  15558  prm23lt5  15566  prm23ge5  15567  dvdsprmpweqnn  15636  dvdsprmpweqle  15637  oddprmdvds  15654  prmpwdvds  15655  prmreclem4  15670  ramcl  15780  prmgaplem6  15807  prmgaplem7  15808  prmgaplem8  15809  cshwshashlem1  15849  cshwshashlem2  15850  cshwshashlem3  15851  cshwrepswhash1  15856  setsn0fun  15942  setsstruct2  15943  setsstructOLD  15946  imasleval  16248  mreiincl  16303  mreexexd  16355  mreexexdOLD  16356  inveq  16481  cicsym  16511  cictr  16512  initoid  16702  termoid  16703  initoeu2lem0  16710  initoeu2lem1  16711  initoeu2lem2  16712  initoeu2  16713  fthestrcsetc  16837  fthsetcestrc  16852  drsdirfi  16985  isnmgm  17293  sgrpass  17337  mgm2nsgrplem3  17454  dfgrp3lem  17560  symg2bas  17864  symgfix2  17882  symgextf1  17887  gsmsymgrfix  17894  pmtrprfv3  17920  psgnunilem4  17963  efgi2  18184  lmodvsmmulgdi  18946  0ringnnzr  19317  mpfrcl  19566  gsummoncoe1  19722  psgndiflemB  19994  psgndiflemA  19995  elfrlmbasn0  20154  lmictra  20232  mamufacex  20243  matecl  20279  dmatelnd  20350  dmatscmcl  20357  scmateALT  20366  scmatsgrp1  20376  scmatf1  20385  mavmulsolcl  20405  cramerimplem1  20537  cramerimplem2  20538  pmatcollpw3fi1  20641  mp2pm2mplem4  20662  pm2mpfo  20667  chmaidscmat  20701  fvmptnn04ifb  20704  chfacfscmul0  20711  chfacfpmmul0  20715  cayhamlem1  20719  cayhamlem3  20740  cayleyhamilton1  20745  fiinopn  20754  toprntopon  20777  tgcl  20821  distop  20847  isclo2  20940  iscldtop  20947  ssnei2  20968  opnnei  20972  pnfnei  21072  mnfnei  21073  tgcnp  21105  cnpnei  21116  1stcelcls  21312  txcnpi  21459  cnmptcom  21529  fbfinnfr  21692  isfildlem  21708  snfil  21715  fbunfip  21720  fgcl  21729  elfm2  21799  fmco  21812  fbflim2  21828  cnpflf2  21851  flimfcls  21877  tmdgsum  21946  neibl  22353  tngngpim  22510  fgcfil  23115  caubl  23152  volsuplem  23369  ellimc3  23688  dvnadd  23737  dvnres  23739  cpnord  23743  dvnfre  23760  ply1divex  23941  cxpmul2  24480  zabsle1  25066  gausslemma2dlem0i  25134  gausslemma2dlem1a  25135  gausslemma2dlem3  25138  lgsquad2lem2  25155  2lgs  25177  qabvexp  25360  axcontlem4  25892  umgredgprv  26047  umgrnloop  26048  upgrpredgv  26079  upgredgpr  26082  edglnl  26083  usgredgprvALT  26132  usgrnloopALT  26140  usgredg2v  26164  fusgrfis  26267  nbuhgr2vtx1edgblem  26292  nb3grprlem1  26326  cusgrsize2inds  26405  cusgrfi  26410  fusgrn0degnn0  26451  uspgrloopvtxel  26468  vtxdginducedm1lem4  26494  uhgr0edg0rgrb  26526  wlkl1loop  26590  wlk1walk  26591  upgriswlk  26593  upgrwlkvtxedg  26597  uspgr2wlkeq  26598  wlkv0  26603  wlklenvclwlk  26607  wlksoneq1eq2  26616  wlkon2n0  26618  wlkreslem  26622  wlkres  26623  lfgrwlkprop  26640  pthdivtx  26681  2pthnloop  26683  spthonepeq  26704  uhgrwkspthlem2  26706  uhgrwkspth  26707  usgr2wlkneq  26708  usgr2trlncl  26712  usgr2pthlem  26715  usgr2pth  26716  cyclnspth  26751  lfgrn1cycl  26753  usgr2trlncrct  26754  uspgrn2crct  26756  crctcshwlkn0lem3  26760  crctcshwlkn0lem5  26762  wwlknp  26791  wspthneq1eq2  26814  0enwwlksnge1  26818  wlklnwwlkln1  26822  wlkiswwlks2  26829  wlkiswwlksupgr2  26831  wlklnwwlkln2lem  26836  wwlksnred  26855  wwlksnext  26856  wwlksnextbi  26857  wwlksnredwwlkn0  26859  wwlksnextwrd  26860  wwlksnextinj  26862  wwlksnextproplem3  26874  wwlksnextprop  26875  wspthsnwspthsnon  26879  wspthsnwspthsnonOLD  26881  wspthsnonn0vne  26882  2pthon3v  26908  umgr2adedgwlkonALT  26912  umgr2wlk  26914  umgr2wlkon  26915  elwwlks2ons3OLD  26921  umgrwwlks2on  26923  elwspths2on  26926  usgr2wspthons3  26931  elwwlks2  26933  rusgrnumwwlk  26942  clwwlknclwwlkdifsOLD  26947  clwlkclwwlklem2a4  26963  clwlkclwwlklem2a  26964  clwlkclwwlklem2  26966  erclwwlkeqlen  26976  clwwlknwwlksn  27000  clwwlknwwlksnOLD  27001  loopclwwlkn1b  27005  clwwlkf1  27012  wwlksext2clwwlk  27021  wwlksext2clwwlkOLD  27022  eleclclwwlknlem2  27026  umgr2cwwk2dif  27028  eleclclwwlkn  27040  hashecclwwlkn1  27041  umgrhashecclwwlk  27042  clwlksfclwwlk  27049  clwlksfoclwwlk  27050  clwwlknonwwlknonb  27080  clwwlknonex2lem2  27083  clwwlknonex2  27084  clwwlknunOLD  27091  1pthon2v  27131  upgr3v3e3cycl  27158  uhgr3cyclexlem  27159  uhgr3cyclex  27160  eupth2lem3lem4  27209  frgr3vlem1  27253  frgr3vlem2  27254  3vfriswmgrlem  27257  3vfriswmgr  27258  3cyclfrgrrn1  27265  n4cyclfrgr  27271  frgrncvvdeqlem3  27281  frgrncvvdeqlem6  27284  frgrncvvdeqlem7  27285  frgrncvvdeqlem8  27286  frgrwopreglem4a  27290  frgrwopreglem3  27294  frgrwopreg1  27298  frgrwopreg2  27299  frgrwopreglem5lem  27300  frgrwopreglem5ALT  27302  frgrwopreg  27303  fusgr2wsp2nb  27314  2wspmdisj  27317  clwwlkccatlem  27331  clwwlkccat  27332  numclwlk1lem2foa  27344  numclwlk1lem2f1  27347  numclwlk1lem2fo  27348  numclwwlk1  27351  numclwwlk2lem1  27356  numclwlk2lem2f  27357  numclwlk2lem2f1o  27359  numclwwlk2lem1OLD  27363  numclwlk2lem2fOLD  27364  numclwlk2lem2f1oOLD  27366  frgrreg  27381  frgrregord013  27382  frgrregord13  27383  friendshipgt3  27385  friendship  27386  eulplig  27467  ipassi  27824  ubthlem2  27855  isch3  28226  shintcli  28316  shmodsi  28376  spansncvi  28639  hoaddsub  28803  eigorthi  28824  pjss2coi  29151  pjnormssi  29155  pj3cor1i  29196  strb  29245  dmdmd  29287  mdsl0  29297  csmdsymi  29321  chrelat2i  29352  mdsymlem3  29392  mdsymlem6  29395  sumdmdlem2  29406  ssrelf  29553  cvmlift2lem1  31410  mrsubvrs  31545  mclsax  31592  3ccased  31726  dfon2lem3  31814  rdgprc  31824  trpredmintr  31855  trpredrec  31862  frr3g  31904  sltval2  31934  nolt02o  31970  sslttr  32039  scutun12  32042  cgrextend  32240  btwndiff  32259  btwnconn1lem12  32330  brsegle  32340  broutsideof2  32354  funray  32372  elicc3  32436  nn0prpwlem  32442  nn0prpw  32443  fnessref  32477  neibastop2lem  32480  filnetlem4  32501  meran1  32535  waj-ax  32538  arg-ax  32540  bj-con2com  32673  bj-axdd2  32701  bj-exalimi  32737  bj-ssbequ2  32768  bj-ssbequ1  32769  bj-ssbid1ALT  32773  bj-sb  32802  bj-cbv1v  32854  bj-dtru  32922  bj-mo3OLD  32957  bj-snsetex  33076  bj-restpw  33170  bj-finsumval0  33277  mptsnunlem  33315  icoreclin  33335  relowlpssretop  33342  wl-dveeq12  33441  wl-dral1d  33448  wl-exeq  33451  wl-lem-exsb  33478  poimirlem29  33568  poimirlem32  33571  fdc  33671  seqpo  33673  incsequz  33674  isismty  33730  ismtybndlem  33735  heibor1lem  33738  ismgmOLD  33779  isexid2  33784  ghomco  33820  pridlc  34000  relcnveq3  34233  elrelscnveq3  34381  cdleme18d  35900  tendovalco  36370  cdlemn11pre  36816  dihord2pre  36831  incssnn0  37591  fphpd  37697  jm2.19lem3  37875  setindtr  37908  islssfg2  37958  mpaaeu  38037  refimssco  38230  iunrelexpmin1  38317  iunrelexpmin2  38321  trclimalb2  38335  clsk1indlem3  38658  syldbl2  38785  nzss  38833  sb5ALT  39048  truniALT  39068  ee223  39176  3orbi123VD  39399  sbc3orgVD  39400  exbirVD  39402  exbiriVD  39403  sbcim2gVD  39425  trsbcVD  39427  truniALTVD  39428  onfrALTlem3VD  39437  onfrALTlem2VD  39439  csbrngVD  39446  19.41rgVD  39452  ax6e2eqVD  39457  ax6e2ndeqVD  39459  2uasbanhVD  39461  sb5ALTVD  39463  vk15.4jVD  39464  infxrunb3rnmpt  39968  stoweidlem26  40561  hirstL-ax3  41380  rexsb  41489  rexrsb  41490  2reu1  41507  afvres  41573  tz6.12-afv  41574  afvco2  41577  zm1nn  41641  fzoopth  41662  2ffzoeq  41663  smonoord  41666  iccpartiltu  41683  iccpartlt  41685  iccpartltu  41686  iccpartgtl  41687  iccpartgt  41688  iccpartleu  41689  iccpartgel  41690  icceuelpart  41697  iccpartnel  41699  lswn0  41705  pfxccatin12lem1  41748  pfxccatin12lem2  41749  pfxccat3  41751  goldbachth  41784  odz2prm2pw  41800  fmtno4prmfac  41809  fmtno4prmfac193  41810  prmdvdsfmtnof1lem2  41822  2pwp1prmfmtno  41829  lighneallem2  41848  lighneallem4b  41851  lighneallem4  41852  odd2prm2  41952  mogoldbblem  41954  gbepos  41971  gbowgt5  41975  gbowge7  41976  stgoldbwt  41989  sbgoldbwt  41990  sbgoldbst  41991  sbgoldbaltlem1  41992  sbgoldbalt  41994  sbgoldbo  42000  nnsum3primesle9  42007  nnsum4primesodd  42009  nnsum4primesoddALTV  42010  nnsum4primeseven  42013  nnsum4primesevenALTV  42014  bgoldbtbndlem1  42018  bgoldbtbndlem2  42019  bgoldbtbndlem3  42020  bgoldbtbnd  42022  upgrwlkupwlk  42046  prsprel  42062  sprsymrelfvlem  42065  sprsymrelf1lem  42066  sprsymrelfolem2  42068  uspgrsprf1  42080  mgmhmlin  42111  issubmgm2  42115  lmod0rng  42193  lidldomn1  42246  lidlmmgm  42250  rnghmsscmap  42299  rnghmsubcsetclem2  42301  rngcinv  42306  rngccatidALTV  42314  rngcinvALTV  42318  funcrngcsetc  42323  funcrngcsetcALT  42324  rhmsscmap  42345  rhmsubcsetclem2  42347  rhmsubcrngclem2  42353  ringcinv  42357  ringcbasbas  42359  funcringcsetc  42360  funcringcsetcALTV2lem9  42369  ringccatidALTV  42377  ringcinvALTV  42381  ringcbasbasALTV  42383  rhmsubclem4  42414  rhmsubcALTVlem4  42432  ztprmneprm  42450  pgrpgt2nabl  42472  lmodvsmdi  42488  ply1mulgsumlem2  42500  lincsumcl  42545  ellcoellss  42549  linindslinci  42562  islinindfis  42563  lincext3  42570  lindslinindimp2lem4  42575  lindslinindsimp2lem5  42576  lindslinindsimp2  42577  lindsrng01  42582  ldepspr  42587  lincresunit3lem1  42593  elfzolborelfzop1  42634  dignn0ldlem  42721  nn0sumshdiglem1  42740  tfis2d  42752  onsetrec  42779
  Copyright terms: Public domain W3C validator