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  356  jaod  395  orel1  397  pm2.62  425  impcom  446  impd  447  expcom  451  expd  452  pm3.21  464  simplbi2com  656  imdistanri  726  pm2.64  829  pm2.75  893  ccased  987  dedlem0b  1000  3impd  1278  3expd  1281  mp3an1i  1414  minimp  1557  meredith  1563  19.35  1802  speimfw  1873  sbequ2  1879  equtrr  1946  equeucl  1948  sb56  2147  axc11nlemOLD  2157  cbv1  2266  axc11nlemALT  2305  axc11n  2306  dvelimdf  2334  ax12b  2344  equvel  2346  sbied  2408  exsb  2467  mo2v  2476  euex  2493  exmoeu  2501  mo3  2506  2mo  2550  2eu6  2557  exists2  2561  rexlimdv  3025  r19.12  3058  2gencl  3226  3gencl  3227  rspccv  3296  ceqex  3321  mob  3375  euind  3380  reuind  3398  sseq2  3612  nelss  3649  reupick2  3895  rspn0  3916  uneqdifeq  4035  uneqdifeqOLD  4036  eqoreldifOLD  4204  ssprsseq  4332  eqsnOLD  4337  preq12b  4357  prel12  4358  prnebg  4364  iinss2  4545  disjxiunOLD  4620  trintss  4739  dtru  4827  reusv1OLD  4837  reusv2lem1  4838  alxfr  4848  ralxfrALT  4857  sspwb  4888  copsexg  4926  propeqop  4940  pocl  5012  pofun  5021  solin  5028  frss  5051  2optocl  5167  3optocl  5168  ssrel  5178  ssrelOLD  5179  ssrel2  5181  ssrelrel  5191  relop  5242  restidsingOLD  5428  asymref2  5482  xpidtr  5487  trin2  5488  poltletr  5497  xp11  5538  relcnvtr  5624  tz7.7  5718  ordtri3OLD  5729  ordtr2  5737  suc11  5800  iotaval  5831  funmo  5873  fundif  5903  fss  6023  f0dom0  6056  fv3  6173  tz6.12c  6180  tz6.12i  6181  mpteqb  6265  fveqdmss  6320  eldmrexrnb  6332  funopsn  6378  funsndifnop  6381  tpres  6431  funfvima  6457  fvclss  6465  f1veqaeq  6479  isoselem  6556  oprabv  6668  ovg  6764  elovmpt3rab1  6858  sorpsscmpl  6913  iunpw  6940  ordom  7036  limom  7042  peano5  7051  fornex  7097  bropopvvv  7215  bropfvvvvlem  7216  f1o2ndf1  7245  poxp  7249  soxp  7250  suppimacnv  7266  ressuppss  7274  ressuppssdif  7276  tposfn2  7334  wfr3g  7373  onnseq  7401  smoel  7417  smogt  7424  smoiso2  7426  tfr3  7455  tz7.48-2  7497  tz7.48-3  7499  tz7.49  7500  oecl  7577  oaordex  7598  oalimcl  7600  oaass  7601  omordi  7606  omlimcl  7618  odi  7619  omeulem1  7622  oen0  7626  nnawordi  7661  nnaass  7662  nnmordi  7671  omabs  7687  omsmolem  7693  iiner  7779  2ecoptocl  7798  3ecoptocl  7799  undifixp  7904  xpdom2  8015  xpf1o  8082  infensuc  8098  php  8104  onomeneq  8110  isinf  8133  findcard2  8160  unblem2  8173  infssuni  8217  finsschain  8233  fsuppunfi  8255  fsuppunbi  8256  marypha1  8300  hartogs  8409  card2on  8419  card2inf  8420  xpwdomg  8450  elirrv  8464  en3lp  8473  inf3lem1  8485  inf3lem2  8486  inf3lem3  8487  inf3lem5  8489  noinfep  8517  trcl  8564  tcel  8581  rankonidlem  8651  scottex  8708  dif1card  8793  fodomnum  8840  cardaleph  8872  kmlem9  8940  kmlem13  8944  cflim2  9045  cfsmolem  9052  infpssrlem3  9087  isfin7-2  9178  fin1a2lem6  9187  fin1a2lem10  9191  fin1a2lem12  9193  domtriomlem  9224  axdc3lem4  9235  axdc4lem  9237  zorn2lem3  9280  zorn2lem4  9281  zorn2lem5  9282  zorn2lem7  9284  zornn0g  9287  axdclem2  9302  ondomon  9345  alephval2  9354  cfpwsdom  9366  wuncval2  9529  grupr  9579  gruiun  9581  ingru  9597  grothomex  9611  indpi  9689  nqereu  9711  prlem934  9815  reclem2pr  9830  mulgt0sr  9886  supsrlem  9892  dedekind  10160  lemul1a  10837  squeeze0  10886  peano5nni  10983  nnunb  11248  nn0lt2  11400  nn0le2is012  11401  fzind  11435  nn0ind-raph  11437  zindd  11438  eluzadd  11676  uzin  11680  nn01to3  11741  xnn0xadd0  12036  xmulasslem  12074  icoshft  12252  fzen  12316  uzsubsubfz  12321  elfz1b  12367  elfz0ubfz0  12400  elfz0fzfz0  12401  fz0fzelfz0  12402  elfzmlbp  12407  elfzodifsumelfzo  12490  ssfzo12bi  12520  elfzonelfzo  12527  elfznelfzo  12530  injresinjlem  12544  injresinj  12545  modfzo0difsn  12698  modsumfzodifsn  12699  addmodlteq  12701  ssnn0fi  12740  fsuppmapnn0fiub0  12749  expcllem  12827  expeq0  12846  mulexp  12855  leexp2r  12874  bernneq  12946  facdiv  13030  hasheqf1oi  13096  hasheqf1oiOLD  13097  hashf1rnOLD  13099  hashnn0n0nn  13136  hashss  13153  hashgt12el  13166  hashgt12el2  13167  hashmap  13178  hashimarni  13182  hash2prde  13206  hashle2pr  13213  pr2pwpr  13215  hashge2el2dif  13216  hashge2el2difr  13217  hashtpg  13221  hashge3el3dif  13222  exprelprel  13226  hash1to3  13228  fundmge2nop0  13229  fi1uzind  13234  fi1uzindOLD  13240  ccatsymb  13321  swrdnd  13386  swrdnd2  13387  swrdswrdlem  13413  swrdswrd  13414  swrdccatin1  13436  swrdccatin12lem2a  13438  swrdccatin12lem2b  13439  swrdccatin2  13440  swrdccatin12lem2  13442  swrdccatin12lem3  13443  swrdccat3  13445  swrdccat  13446  swrdccat3blem  13448  repsdf2  13478  repswswrd  13484  cshwidxmod  13502  cshwidx0  13505  cshf1  13509  2cshw  13512  cshweqrep  13520  cshw1  13521  cshwsexa  13523  2cshwcshw  13524  scshwfzeqfzo  13525  cshwcsh2id  13527  swrdco  13536  wwlktovfo  13651  relexpaddg  13743  cjexp  13840  absexp  13994  iseraltlem2  14363  modfsummods  14471  clim2prod  14564  prodfn0  14570  prodfrec  14571  prodmo  14610  fprodabs  14648  binomfallfac  14716  fprodefsum  14769  dvdsaddre2b  14972  addmodlteqALT  14990  oddge22np1  15016  nn0enne  15037  nn0o1gt2  15040  sumeven  15053  sumodd  15054  dvdslegcd  15169  gcdneg  15186  dfgcd2  15206  rplpwr  15219  lcmf  15289  lcmftp  15292  lcmfunsnlem2lem1  15294  lcmfunsnlem2  15296  lcmfdvds  15298  lcmfdvdsb  15299  lcmfunsn  15300  coprmdvds1  15308  qredeq  15314  coprmprod  15318  coprmproddvdslem  15319  cncongr1  15324  cncongr2  15325  prm2orodd  15347  nnnn0modprm0  15454  prm23lt5  15462  prm23ge5  15463  dvdsprmpweqnn  15532  dvdsprmpweqle  15533  oddprmdvds  15550  prmpwdvds  15551  prmreclem4  15566  ramcl  15676  prmgaplem6  15703  prmgaplem7  15704  prmgaplem8  15705  cshwshashlem1  15745  cshwshashlem2  15746  cshwshashlem3  15747  cshwrepswhash1  15752  setsn0fun  15835  setsstruct2  15836  setsstructOLD  15839  imasleval  16141  mreiincl  16196  mreexexd  16248  mreexexdOLD  16249  inveq  16374  cicsym  16404  cictr  16405  initoid  16595  termoid  16596  initoeu2lem0  16603  initoeu2lem1  16604  initoeu2lem2  16605  initoeu2  16606  fthestrcsetc  16730  fthsetcestrc  16745  drsdirfi  16878  isnmgm  17186  sgrpass  17230  mgm2nsgrplem3  17347  dfgrp3lem  17453  symg2bas  17758  symgfix2  17776  symgextf1  17781  gsmsymgrfix  17788  pmtrprfv3  17814  psgnunilem4  17857  efgi2  18078  lmodvsmmulgdi  18838  0ringnnzr  19209  mpfrcl  19458  gsummoncoe1  19614  psgndiflemB  19886  psgndiflemA  19887  elfrlmbasn0  20046  lmictra  20124  mamufacex  20135  matecl  20171  dmatelnd  20242  dmatscmcl  20249  scmateALT  20258  scmatsgrp1  20268  scmatf1  20277  mavmulsolcl  20297  cramerimplem1  20429  cramerimplem2  20430  pmatcollpw3fi1  20533  mp2pm2mplem4  20554  pm2mpfo  20559  chmaidscmat  20593  fvmptnn04ifb  20596  chfacfscmul0  20603  chfacfpmmul0  20607  cayhamlem1  20611  cayhamlem3  20632  cayleyhamilton1  20637  fiinopn  20646  toprntopon  20669  tgcl  20713  distop  20739  isclo2  20832  iscldtop  20839  ssnei2  20860  opnnei  20864  pnfnei  20964  mnfnei  20965  tgcnp  20997  cnpnei  21008  1stcelcls  21204  txcnpi  21351  cnmptcom  21421  fbfinnfr  21585  isfildlem  21601  snfil  21608  fbunfip  21613  fgcl  21622  elfm2  21692  fmco  21705  fbflim2  21721  cnpflf2  21744  flimfcls  21770  tmdgsum  21839  neibl  22246  tngngpim  22403  fgcfil  23009  caubl  23046  volsuplem  23263  ellimc3  23583  dvnadd  23632  dvnres  23634  cpnord  23638  dvnfre  23655  ply1divex  23834  cxpmul2  24369  zabsle1  24955  lgsqrmodndvds  25012  gausslemma2dlem0i  25023  gausslemma2dlem1a  25024  gausslemma2dlem3  25027  lgsquad2lem2  25044  2lgs  25066  qabvexp  25249  axcontlem4  25781  umgredgprv  25931  umgrnloop  25932  upgrpredgv  25963  upgredgpr  25966  usgredgprvALT  26014  usgrnloopALT  26022  usgredg2v  26046  fusgrfis  26144  nbuhgr2vtx1edgblem  26168  nb3grprlem1  26203  cusgrsize2inds  26270  cusgrfi  26275  fusgrn0degnn0  26315  uspgrloopvtxel  26332  uhgr0edg0rgrb  26374  wlkl1loop  26437  wlk1walk  26438  upgriswlk  26440  upgrwlkvtxedg  26444  uspgr2wlkeq  26445  wlkv0  26450  wlklenvclwlk  26454  wlksoneq1eq2  26463  wlkon2n0  26465  wlkreslem  26469  wlkres  26470  lfgrwlkprop  26487  pthdivtx  26528  2pthnloop  26530  spthonepeq  26551  uhgrwkspthlem2  26553  uhgrwkspth  26554  usgr2wlkneq  26555  usgr2trlncl  26559  usgr2pthlem  26562  usgr2pth  26563  cyclnspth  26598  lfgrn1cycl  26600  usgr2trlncrct  26601  uspgrn2crct  26603  crctcshwlkn0lem3  26607  crctcshwlkn0lem5  26609  wwlknp  26637  wspthneq1eq2  26648  0enwwlksnge1  26652  wlklnwwlkln1  26657  wlkiswwlks2  26664  wlkiswwlksupgr2  26666  wlklnwwlkln2lem  26671  wwlksnred  26690  wwlksnext  26691  wwlksnextbi  26692  wwlksnredwwlkn0  26694  wwlksnextwrd  26695  wwlksnextinj  26697  wwlksnextproplem3  26709  wwlksnextprop  26710  wspthsnwspthsnon  26714  wspthsnonn0vne  26716  wspn0  26723  2pthon3v  26742  umgr2adedgwlkonALT  26746  umgr2wlk  26748  umgr2wlkon  26749  elwwlks2ons3  26751  umgrwwlks2on  26753  elwspths2on  26755  usgr2wspthons3  26759  elwwlks2  26762  rusgrnumwwlk  26771  clwwlknclwwlkdifs  26774  clwwlknp  26788  clwlkclwwlklem2a4  26799  clwlkclwwlklem2a  26800  clwlkclwwlklem2  26802  clwwlksf1  26817  wwlksext2clwwlk  26824  erclwwlkseqlen  26833  eleclclwwlksnlem2  26839  umgr2cwwk2dif  26841  eleclclwwlksn  26853  hashecclwwlksn1  26854  umgrhashecclwwlk  26855  clwlksfclwwlk  26862  clwlksfoclwwlk  26863  clwwlksnun  26874  1pthon2v  26913  upgr3v3e3cycl  26940  uhgr3cyclexlem  26941  uhgr3cyclex  26942  eupth2lem3lem4  26991  frgr3vlem1  27035  frgr3vlem2  27036  3vfriswmgrlem  27039  3vfriswmgr  27040  3cyclfrgrrn1  27047  n4cyclfrgr  27053  frgrncvvdeqlem2  27062  frgrncvvdeqlem3  27063  frgrncvvdeqlem4  27064  frgrncvvdeqlem7  27067  frgrncvvdeqlemA  27068  frgrncvvdeqlemB  27069  frgrncvvdeqlemC  27070  frgrwopreglem3  27075  frgrwopreglem4  27076  frgrwopreglem5  27077  frgrwopreg  27078  frgrwopreg1  27079  frgrwopreg2  27080  frgr2wwlk1  27086  frgr2wwlkeqm  27088  fusgr2wsp2nb  27090  frrusgrord0  27095  extwwlkfablem2  27102  numclwwlkovf2ex  27109  numclwlk1lem2foa  27113  numclwlk1lem2f1  27116  numclwlk1lem2fo  27117  numclwwlk1  27120  numclwwlk2lem1  27124  numclwlk2lem2f  27125  numclwlk2lem2f1o  27127  frgrreg  27140  frgrregord013  27141  frgrregord13  27142  friendshipgt3  27144  friendship  27145  eulplig  27225  ipassi  27584  ubthlem2  27615  isch3  27986  shintcli  28076  shmodsi  28136  spansncvi  28399  hoaddsub  28563  eigorthi  28584  pjss2coi  28911  pjnormssi  28915  pj3cor1i  28956  strb  29005  dmdmd  29047  mdsl0  29057  csmdsymi  29081  chrelat2i  29112  mdsymlem3  29152  mdsymlem6  29155  sumdmdlem2  29166  ssrelf  29309  cvmlift2lem1  31045  mrsubvrs  31180  mclsax  31227  3ccased  31362  dfres3  31410  dfon2lem3  31444  rdgprc  31454  trpredmintr  31485  trpredrec  31492  frr3g  31533  sltval2  31563  cgrextend  31810  btwndiff  31829  btwnconn1lem12  31900  brsegle  31910  broutsideof2  31924  funray  31942  elicc3  32006  nn0prpwlem  32012  nn0prpw  32013  fnessref  32047  neibastop2lem  32050  filnetlem4  32071  meran1  32105  waj-ax  32108  arg-ax  32110  bj-con2com  32243  bj-axdd2  32271  bj-exalimi  32307  bj-ssbequ2  32338  bj-ssbequ1  32339  bj-ssbid1ALT  32343  bj-sb  32372  bj-cbv1v  32424  bj-dtru  32493  bj-mo3OLD  32530  bj-snsetex  32651  bj-restpw  32735  bj-finsumval0  32819  mptsnunlem  32856  icoreclin  32876  relowlpssretop  32883  wl-dveeq12  32982  wl-dral1d  32989  wl-exeq  32992  wl-lem-exsb  33019  poimirlem29  33109  poimirlem32  33112  fdc  33212  seqpo  33214  incsequz  33215  isismty  33271  ismtybndlem  33276  heibor1lem  33279  ismgmOLD  33320  isexid2  33325  ghomco  33361  pridlc  33541  cdleme18d  35101  tendovalco  35572  cdlemn11pre  36018  dihord2pre  36033  incssnn0  36793  fphpd  36899  jm2.19lem3  37077  setindtr  37110  islssfg2  37160  mpaaeu  37240  refimssco  37433  iunrelexpmin1  37520  iunrelexpmin2  37524  trclimalb2  37538  clsk1indlem3  37862  syldbl2  37989  nzss  38037  sb5ALT  38252  truniALT  38272  ee223  38380  3orbi123VD  38607  sbc3orgVD  38608  exbirVD  38610  exbiriVD  38611  sbcim2gVD  38633  trsbcVD  38635  truniALTVD  38636  onfrALTlem3VD  38645  onfrALTlem2VD  38647  csbrngVD  38654  19.41rgVD  38660  ax6e2eqVD  38665  ax6e2ndeqVD  38667  2uasbanhVD  38669  sb5ALTVD  38671  vk15.4jVD  38672  infxrunb3rnmpt  39154  stoweidlem26  39580  hirstL-ax3  40393  rexsb  40502  rexrsb  40503  2reu1  40520  afvres  40586  tz6.12-afv  40587  afvco2  40590  zm1nn  40643  fzoopth  40664  2ffzoeq  40665  smonoord  40669  iccpartiltu  40686  iccpartlt  40688  iccpartltu  40689  iccpartgtl  40690  iccpartgt  40691  iccpartleu  40692  iccpartgel  40693  icceuelpart  40700  iccpartnel  40702  lswn0  40708  pfxccatin12lem1  40752  pfxccatin12lem2  40753  pfxccat3  40755  goldbachth  40788  odz2prm2pw  40804  fmtno4prmfac  40813  fmtno4prmfac193  40814  prmdvdsfmtnof1lem2  40826  2pwp1prmfmtno  40833  lighneallem2  40852  lighneallem4b  40855  lighneallem4  40856  gbepos  40971  gbogt5  40975  gboge7  40976  stgoldbwt  40989  bgoldbwt  40990  bgoldbst  40991  sgoldbaltlem1  40992  sgoldbalt  40994  nnsum3primesle9  41001  nnsum4primesodd  41003  nnsum4primesoddALTV  41004  nnsum4primeseven  41007  nnsum4primesevenALTV  41008  bgoldbtbndlem1  41012  bgoldbtbndlem2  41013  bgoldbtbndlem3  41014  bgoldbtbnd  41016  upgrwlkupwlk  41039  prsprel  41055  sprsymrelfvlem  41058  sprsymrelf1lem  41059  sprsymrelfolem2  41061  uspgrsprf1  41073  mgmhmlin  41104  issubmgm2  41108  lmod0rng  41186  lidldomn1  41239  lidlmmgm  41243  rnghmsscmap  41292  rnghmsubcsetclem2  41294  rngcinv  41299  rngccatidALTV  41307  rngcinvALTV  41311  funcrngcsetc  41316  funcrngcsetcALT  41317  rhmsscmap  41338  rhmsubcsetclem2  41340  rhmsubcrngclem2  41346  ringcinv  41350  ringcbasbas  41352  funcringcsetc  41353  funcringcsetcALTV2lem9  41362  ringccatidALTV  41370  ringcinvALTV  41374  ringcbasbasALTV  41376  rhmsubclem4  41407  rhmsubcALTVlem4  41425  ztprmneprm  41443  pgrpgt2nabl  41465  lmodvsmdi  41481  ply1mulgsumlem2  41493  lincsumcl  41538  ellcoellss  41542  linindslinci  41555  islinindfis  41556  lincext3  41563  lindslinindimp2lem4  41568  lindslinindsimp2lem5  41569  lindslinindsimp2  41570  lindsrng01  41575  ldepspr  41580  lincresunit3lem1  41586  elfzolborelfzop1  41627  dignn0ldlem  41718  nn0sumshdiglem1  41737  tfis2d  41749  onsetrec  41774
  Copyright terms: Public domain W3C validator