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  658  imdistanri  729  pm2.64  865  pm2.75  930  ccased  1025  dedlem0b  1031  3impd  1442  3expd  1447  mp3an1i  1566  minimp  1709  meredith  1715  19.35  1954  speimfw  2042  sbequ2  2048  equtrr  2104  equeucl  2106  sb56  2297  cbv1  2412  axc11n  2451  dvelimdf  2475  ax12b  2482  equvel  2484  sbied  2546  exsb  2605  mo2v  2614  euex  2631  exmoeu  2640  mo3  2645  2mo  2689  2eu6  2696  exists2  2700  rexlimdv  3168  r19.12  3201  2gencl  3376  3gencl  3377  rspccv  3446  ceqex  3472  mob  3529  euind  3534  reuind  3552  sseq2  3768  nelss  3805  reupick2  4056  rspn0  4077  disjeq0  4166  uneqdifeq  4201  uneqdifeqOLD  4202  eqoreldifOLD  4370  ssprsseq  4502  eqsnOLD  4507  preq12b  4526  prel12OLD  4527  prnebg  4533  prel12g  4544  3elpr2eq  4587  iinss2  4724  trintss  4921  dtru  5006  reusv1OLD  5016  reusv2lem1  5017  alxfr  5027  ralxfrALT  5036  sspwb  5066  copsexg  5104  propeqop  5118  opthhausdorff  5127  opthhausdorff0  5128  pocl  5194  pofun  5203  solin  5210  frss  5233  2optocl  5353  3optocl  5354  ssrel  5364  ssrelOLD  5365  ssrel2  5367  ssrelrel  5377  relop  5428  dfres3  5556  restidsingOLD  5617  asymref2  5671  xpidtr  5676  trin2  5677  poltletr  5686  xp11  5727  relcnvtr  5816  tz7.7  5910  ordtri3OLD  5921  ordtr2  5929  suc11  5992  iotaval  6023  funmo  6065  fundif  6096  fss  6217  f0dom0  6250  fv3  6367  tz6.12c  6374  tz6.12i  6375  mpteqb  6461  fveqdmss  6517  eldmrexrnb  6529  funopsn  6576  funsndifnop  6579  tpres  6630  funfvima  6655  fvclss  6663  f1veqaeq  6677  isoselem  6754  oprabv  6868  ovg  6964  elovmpt3rab1  7058  sorpsscmpl  7113  iunpw  7143  ordom  7239  limom  7245  peano5  7254  fornex  7300  bropopvvv  7423  bropfvvvvlem  7424  f1o2ndf1  7453  poxp  7457  soxp  7458  suppimacnv  7474  ressuppss  7482  ressuppssdif  7484  tposfn2  7543  wfr3g  7582  onnseq  7610  smoel  7626  smogt  7633  smoiso2  7635  tfr3  7664  tz7.48-2  7706  tz7.48-3  7708  tz7.49  7709  oecl  7786  oaordex  7807  oalimcl  7809  oaass  7810  omordi  7815  omlimcl  7827  odi  7828  omeulem1  7831  oen0  7835  nnawordi  7870  nnaass  7871  nnmordi  7880  omabs  7896  omsmolem  7902  iiner  7986  2ecoptocl  8005  3ecoptocl  8006  undifixp  8110  xpdom2  8220  xpf1o  8287  infensuc  8303  php  8309  onomeneq  8315  isinf  8338  findcard2  8365  unblem2  8378  infssuni  8422  finsschain  8438  fsuppunfi  8460  fsuppunbi  8461  marypha1  8505  hartogs  8614  card2on  8624  card2inf  8625  xpwdomg  8655  elirrv  8666  en3lp  8682  preleqg  8683  inf3lem1  8698  inf3lem2  8699  inf3lem3  8700  inf3lem5  8702  noinfep  8730  trcl  8777  tcel  8794  rankonidlem  8864  scottex  8921  dif1card  9023  fodomnum  9070  cardaleph  9102  kmlem9  9172  kmlem13  9176  cflim2  9277  cfsmolem  9284  infpssrlem3  9319  isfin7-2  9410  fin1a2lem6  9419  fin1a2lem10  9423  fin1a2lem12  9425  domtriomlem  9456  axdc3lem4  9467  axdc4lem  9469  zorn2lem3  9512  zorn2lem4  9513  zorn2lem5  9514  zorn2lem7  9516  zornn0g  9519  axdclem2  9534  ondomon  9577  alephval2  9586  cfpwsdom  9598  wuncval2  9761  grupr  9811  gruiun  9813  ingru  9829  grothomex  9843  indpi  9921  nqereu  9943  prlem934  10047  reclem2pr  10062  mulgt0sr  10118  supsrlem  10124  dedekind  10392  lemul1a  11069  squeeze0  11118  peano5nni  11215  nnunb  11480  nn0lt2  11632  nn0le2is012  11633  fzind  11667  nn0ind-raph  11669  zindd  11670  eluzadd  11908  uzin  11913  nn01to3  11974  xnn0xadd0  12270  xmulasslem  12308  icoshft  12487  fzen  12551  uzsubsubfz  12556  elfz0ubfz0  12637  elfz0fzfz0  12638  fz0fzelfz0  12639  elfzmlbp  12644  elfzodifsumelfzo  12728  ssfzo12bi  12757  elfzonelfzo  12764  elfznelfzo  12767  injresinjlem  12782  injresinj  12783  modfzo0difsn  12936  modsumfzodifsn  12937  addmodlteq  12939  ssnn0fi  12978  fsuppmapnn0fiub0  12987  expcllem  13065  expeq0  13084  mulexp  13093  leexp2r  13112  bernneq  13184  facdiv  13268  hasheqf1oi  13334  hashnn0n0nn  13372  hashss  13389  hashgt12el  13402  hashgt12el2  13403  hashmap  13414  hashimarni  13420  hash2prde  13444  hashle2pr  13451  pr2pwpr  13453  hashge2el2dif  13454  hashge2el2difr  13455  hashtpg  13459  hashge3el3dif  13460  exprelprel  13463  hash1to3  13465  fundmge2nop0  13466  fi1uzind  13471  ccatsymb  13554  swrdnd  13632  swrdnd2  13633  swrdswrdlem  13659  swrdswrd  13660  swrdccatin1  13683  swrdccatin12lem2a  13685  swrdccatin12lem2b  13686  swrdccatin2  13687  swrdccatin12lem2  13689  swrdccatin12lem3  13690  swrdccat3  13692  swrdccat  13693  swrdccat3blem  13695  repsdf2  13725  repswswrd  13731  cshwidxmod  13749  cshwidx0  13752  cshf1  13756  2cshw  13759  cshweqrep  13767  cshw1  13768  cshwsexa  13770  2cshwcshw  13771  scshwfzeqfzo  13772  cshwcsh2id  13774  swrdco  13783  wwlktovfo  13902  relexpaddg  13992  cjexp  14089  absexp  14243  iseraltlem2  14612  modfsummods  14724  clim2prod  14819  prodfn0  14825  prodfrec  14826  prodmo  14865  fprodabs  14903  binomfallfac  14971  fprodefsum  15024  dvdsaddre2b  15231  addmodlteqALT  15249  oddge22np1  15275  nn0enne  15296  nn0o1gt2  15299  sumeven  15312  sumodd  15313  dvdslegcd  15428  gcdneg  15445  dfgcd2  15465  rplpwr  15478  lcmf  15548  lcmftp  15551  lcmfunsnlem2lem1  15553  lcmfunsnlem2  15555  lcmfdvds  15557  lcmfdvdsb  15558  lcmfunsn  15559  coprmdvds1  15567  qredeq  15573  coprmprod  15577  coprmproddvdslem  15578  cncongr1  15583  cncongr2  15584  prm2orodd  15606  nnnn0modprm0  15713  prm23lt5  15721  prm23ge5  15722  dvdsprmpweqnn  15791  dvdsprmpweqle  15792  oddprmdvds  15809  prmpwdvds  15810  prmreclem4  15825  ramcl  15935  prmgaplem6  15962  prmgaplem7  15963  prmgaplem8  15964  cshwshashlem1  16004  cshwshashlem2  16005  cshwshashlem3  16006  cshwrepswhash1  16011  setsn0fun  16097  setsstruct2  16098  setsstructOLD  16101  imasleval  16403  mreiincl  16458  mreexexd  16510  inveq  16635  cicsym  16665  cictr  16666  initoid  16856  termoid  16857  initoeu2lem0  16864  initoeu2lem1  16865  initoeu2lem2  16866  initoeu2  16867  fthestrcsetc  16991  fthsetcestrc  17006  drsdirfi  17139  isnmgm  17447  sgrpass  17491  mgm2nsgrplem3  17608  dfgrp3lem  17714  symg2bas  18018  symgfix2  18036  symgextf1  18041  gsmsymgrfix  18048  pmtrprfv3  18074  psgnunilem4  18117  efgi2  18338  lmodvsmmulgdi  19100  0ringnnzr  19471  mpfrcl  19720  gsummoncoe1  19876  psgndiflemB  20148  psgndiflemA  20149  elfrlmbasn0  20308  lmictra  20386  mamufacex  20397  matecl  20433  dmatelnd  20504  dmatscmcl  20511  scmateALT  20520  scmatsgrp1  20530  scmatf1  20539  mavmulsolcl  20559  cramerimplem1  20691  cramerimplem2  20692  pmatcollpw3fi1  20795  mp2pm2mplem4  20816  pm2mpfo  20821  chmaidscmat  20855  fvmptnn04ifb  20858  chfacfscmul0  20865  chfacfpmmul0  20869  cayhamlem1  20873  cayhamlem3  20894  cayleyhamilton1  20899  fiinopn  20908  toprntopon  20931  tgcl  20975  distop  21001  isclo2  21094  iscldtop  21101  ssnei2  21122  opnnei  21126  pnfnei  21226  mnfnei  21227  tgcnp  21259  cnpnei  21270  1stcelcls  21466  txcnpi  21613  cnmptcom  21683  fbfinnfr  21846  isfildlem  21862  snfil  21869  fbunfip  21874  fgcl  21883  elfm2  21953  fmco  21966  fbflim2  21982  cnpflf2  22005  flimfcls  22031  tmdgsum  22100  neibl  22507  tngngpim  22664  fgcfil  23269  caubl  23306  volsuplem  23523  ellimc3  23842  dvnadd  23891  dvnres  23893  cpnord  23897  dvnfre  23914  ply1divex  24095  cxpmul2  24634  zabsle1  25220  gausslemma2dlem0i  25288  gausslemma2dlem1a  25289  gausslemma2dlem3  25292  lgsquad2lem2  25309  2lgs  25331  qabvexp  25514  axcontlem4  26046  umgredgprv  26201  umgrnloop  26202  upgrpredgv  26233  upgredgpr  26236  edglnl  26237  usgredgprvALT  26286  usgrnloopALT  26294  usgredg2v  26318  fusgrfis  26421  nbuhgr2vtx1edgblem  26446  nb3grprlem1  26480  cusgrsize2inds  26559  cusgrfi  26564  fusgrn0degnn0  26605  uspgrloopvtxel  26622  vtxdginducedm1lem4  26648  uhgr0edg0rgrb  26680  wlkl1loop  26744  wlk1walk  26745  upgriswlk  26747  upgrwlkvtxedg  26751  uspgr2wlkeq  26752  wlkv0  26757  wlklenvclwlk  26761  wlksoneq1eq2  26770  wlkon2n0  26772  wlkreslem  26776  wlkres  26777  lfgrwlkprop  26794  pthdivtx  26835  2pthnloop  26837  spthonepeq  26858  uhgrwkspthlem2  26860  uhgrwkspth  26861  usgr2wlkneq  26862  usgr2trlncl  26866  usgr2pthlem  26869  usgr2pth  26870  cyclnspth  26906  lfgrn1cycl  26908  usgr2trlncrct  26909  uspgrn2crct  26911  crctcshwlkn0lem3  26915  crctcshwlkn0lem5  26917  wwlknp  26946  wspthneq1eq2  26969  0enwwlksnge1  26973  wlklnwwlkln1  26977  wlkiswwlks2  26984  wlkiswwlksupgr2  26986  wlklnwwlkln2lem  26991  wwlksnred  27010  wwlksnext  27011  wwlksnextbi  27012  wwlksnredwwlkn0  27014  wwlksnextwrd  27015  wwlksnextinj  27017  wwlksnextproplem3  27029  wwlksnextprop  27030  wspthsnwspthsnon  27034  wspthsnwspthsnonOLD  27036  wspthsnonn0vne  27037  2pthon3v  27063  umgr2adedgwlkonALT  27067  umgr2wlk  27069  umgr2wlkon  27070  elwwlks2ons3OLD  27076  umgrwwlks2on  27078  elwspths2on  27081  usgr2wspthons3  27086  elwwlks2  27088  rusgrnumwwlk  27097  clwwlknclwwlkdifsOLD  27102  clwwlkccatlem  27112  clwwlkccat  27113  clwlkclwwlklem2a4  27120  clwlkclwwlklem2a  27121  clwlkclwwlklem2  27123  clwlkclwwlkf1lem3  27129  erclwwlkeqlen  27142  clwwlknwwlksn  27166  clwwlknwwlksnOLD  27167  loopclwwlkn1b  27171  clwwlkf1  27178  wwlksext2clwwlk  27187  wwlksext2clwwlkOLD  27188  eleclclwwlknlem2  27192  umgr2cwwk2dif  27195  eleclclwwlkn  27207  hashecclwwlkn1  27208  umgrhashecclwwlk  27209  clwlksfclwwlkOLD  27216  clwlksfoclwwlkOLD  27217  clwwlknonwwlknonb  27254  clwwlknonex2lem2  27257  clwwlknonex2  27258  clwwlknunOLD  27265  1pthon2v  27305  upgr3v3e3cycl  27332  uhgr3cyclexlem  27333  uhgr3cyclex  27334  eupth2lem3lem4  27383  frgr3vlem1  27427  frgr3vlem2  27428  3vfriswmgrlem  27431  3vfriswmgr  27432  3cyclfrgrrn1  27439  n4cyclfrgr  27445  frgrncvvdeqlem3  27455  frgrncvvdeqlem6  27458  frgrncvvdeqlem7  27459  frgrncvvdeqlem8  27460  frgrwopreglem4a  27464  frgrwopreglem3  27468  frgrwopreg1  27472  frgrwopreg2  27473  frgrwopreglem5lem  27474  frgrwopreglem5ALT  27476  frgrwopreg  27477  fusgr2wsp2nb  27488  2wspmdisj  27491  numclwlk1lem2foa  27513  numclwlk1lem2f1  27516  numclwlk1lem2fo  27517  numclwwlk1  27520  wlkl0  27528  numclwwlk2lem1  27537  numclwlk2lem2f  27538  numclwlk2lem2f1o  27540  numclwwlk2lem1OLD  27544  numclwlk2lem2fOLD  27545  numclwlk2lem2f1oOLD  27547  frgrreg  27562  frgrregord013  27563  frgrregord13  27564  friendshipgt3  27566  friendship  27567  eulplig  27648  ipassi  28005  ubthlem2  28036  isch3  28407  shintcli  28497  shmodsi  28557  spansncvi  28820  hoaddsub  28984  eigorthi  29005  pjss2coi  29332  pjnormssi  29336  pj3cor1i  29377  strb  29426  dmdmd  29468  mdsl0  29478  csmdsymi  29502  chrelat2i  29533  mdsymlem3  29573  mdsymlem6  29576  sumdmdlem2  29587  ssrelf  29734  cvmlift2lem1  31591  mrsubvrs  31726  mclsax  31773  3ccased  31907  dfon2lem3  31995  rdgprc  32005  trpredmintr  32036  trpredrec  32043  frr3g  32085  sltval2  32115  nolt02o  32151  sslttr  32220  scutun12  32223  cgrextend  32421  btwndiff  32440  btwnconn1lem12  32511  brsegle  32521  broutsideof2  32535  funray  32553  elicc3  32617  nn0prpwlem  32623  nn0prpw  32624  fnessref  32658  neibastop2lem  32661  filnetlem4  32682  meran1  32716  waj-ax  32719  arg-ax  32721  bj-con2com  32854  bj-axdd2  32882  bj-exalimi  32918  bj-ssbequ2  32949  bj-ssbequ1  32950  bj-ssbid1ALT  32954  bj-sb  32983  bj-cbv1v  33035  bj-dtru  33103  bj-mo3OLD  33138  bj-snsetex  33257  bj-restpw  33351  bj-finsumval0  33458  mptsnunlem  33496  icoreclin  33516  relowlpssretop  33523  wl-dveeq12  33624  wl-dral1d  33631  wl-exeq  33634  wl-lem-exsb  33661  poimirlem29  33751  poimirlem32  33754  fdc  33854  seqpo  33856  incsequz  33857  isismty  33913  ismtybndlem  33918  heibor1lem  33921  ismgmOLD  33962  isexid2  33967  ghomco  34003  pridlc  34183  relcnveq3  34416  elrelscnveq3  34564  cdleme18d  36085  tendovalco  36555  cdlemn11pre  37001  dihord2pre  37016  incssnn0  37776  fphpd  37882  jm2.19lem3  38060  setindtr  38093  islssfg2  38143  mpaaeu  38222  refimssco  38415  iunrelexpmin1  38502  iunrelexpmin2  38506  trclimalb2  38520  clsk1indlem3  38843  syldbl2  38970  nzss  39018  sb5ALT  39233  truniALT  39253  ee223  39361  3orbi123VD  39584  sbc3orgVD  39585  exbirVD  39587  exbiriVD  39588  sbcim2gVD  39610  trsbcVD  39612  truniALTVD  39613  onfrALTlem3VD  39622  onfrALTlem2VD  39624  csbrngVD  39631  19.41rgVD  39637  ax6e2eqVD  39642  ax6e2ndeqVD  39644  2uasbanhVD  39646  sb5ALTVD  39648  vk15.4jVD  39649  infxrunb3rnmpt  40153  stoweidlem26  40746  hirstL-ax3  41565  rexsb  41674  rexrsb  41675  2reu1  41692  afvres  41758  tz6.12-afv  41759  afvco2  41762  zm1nn  41826  fzoopth  41847  2ffzoeq  41848  smonoord  41851  iccpartiltu  41868  iccpartlt  41870  iccpartltu  41871  iccpartgtl  41872  iccpartgt  41873  iccpartleu  41874  iccpartgel  41875  icceuelpart  41882  iccpartnel  41884  lswn0  41890  pfxccatin12lem1  41933  pfxccatin12lem2  41934  pfxccat3  41936  goldbachth  41969  odz2prm2pw  41985  fmtno4prmfac  41994  fmtno4prmfac193  41995  prmdvdsfmtnof1lem2  42007  2pwp1prmfmtno  42014  lighneallem2  42033  lighneallem4b  42036  lighneallem4  42037  odd2prm2  42137  mogoldbblem  42139  gbepos  42156  gbowgt5  42160  gbowge7  42161  stgoldbwt  42174  sbgoldbwt  42175  sbgoldbst  42176  sbgoldbaltlem1  42177  sbgoldbalt  42179  sbgoldbo  42185  nnsum3primesle9  42192  nnsum4primesodd  42194  nnsum4primesoddALTV  42195  nnsum4primeseven  42198  nnsum4primesevenALTV  42199  bgoldbtbndlem1  42203  bgoldbtbndlem2  42204  bgoldbtbndlem3  42205  bgoldbtbnd  42207  upgrwlkupwlk  42231  prsprel  42247  sprsymrelfvlem  42250  sprsymrelf1lem  42251  sprsymrelfolem2  42253  uspgrsprf1  42265  mgmhmlin  42296  issubmgm2  42300  lmod0rng  42378  lidldomn1  42431  lidlmmgm  42435  rnghmsscmap  42484  rnghmsubcsetclem2  42486  rngcinv  42491  rngccatidALTV  42499  rngcinvALTV  42503  funcrngcsetc  42508  funcrngcsetcALT  42509  rhmsscmap  42530  rhmsubcsetclem2  42532  rhmsubcrngclem2  42538  ringcinv  42542  ringcbasbas  42544  funcringcsetc  42545  funcringcsetcALTV2lem9  42554  ringccatidALTV  42562  ringcinvALTV  42566  ringcbasbasALTV  42568  rhmsubclem4  42599  rhmsubcALTVlem4  42617  ztprmneprm  42635  pgrpgt2nabl  42657  lmodvsmdi  42673  ply1mulgsumlem2  42685  lincsumcl  42730  ellcoellss  42734  linindslinci  42747  islinindfis  42748  lincext3  42755  lindslinindimp2lem4  42760  lindslinindsimp2lem5  42761  lindslinindsimp2  42762  lindsrng01  42767  ldepspr  42772  lincresunit3lem1  42778  elfzolborelfzop1  42819  dignn0ldlem  42906  nn0sumshdiglem1  42925  tfis2d  42937  onsetrec  42964
  Copyright terms: Public domain W3C validator