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.86i  110  pm2.24  124  con3rr3  158  expt  178  jad  188  pm2.61  193  syl5ibcom  246  syl5ibrcom  248  pm5.501  368  impcom  408  impd  411  expcom  414  expdcom  415  simplbi2com  503  imdistanri  570  jaod  853  orel1  882  pm2.62  893  pm2.75  927  pm2.64  935  ccased  1030  dedlem0b  1036  3impd  1340  3expd  1345  mp3an1i  1445  norassOLD  1525  minimp  1613  meredith  1633  19.35  1869  speimfw  1957  equtrr  2020  equeucl  2022  sb56OLD  2269  sbiedw  2323  sbiedwOLD  2324  cbv1v  2347  exsb  2369  cbv1  2413  ax12b  2438  axc11n  2440  dvelimdf  2463  equvel  2471  dfsb1  2503  sbequ2OLDOLD  2507  sbied  2538  sbequ2ALT  2573  sbiedALT  2607  dfmoeu  2611  mo3  2641  mo4  2643  2mo  2726  2eu6  2737  exists2  2742  rexlimdv  3280  r19.12  3321  r19.12OLD  3324  r19.35  3338  2gencl  3533  3gencl  3534  vtocl2ga  3572  rspccv  3617  ceqex  3642  mob  3705  euind  3712  reuind  3741  2reu1  3878  sseq2  3990  nelss  4027  rexdifi  4119  reupick2  4286  rspn0  4310  disjeq0  4401  uneqdifeq  4434  ssprsseq  4750  preq12b  4773  prnebg  4778  prel12g  4786  3elpr2eq  4829  iinss2  4972  trintss  5180  dtru  5262  reusv2lem1  5289  alxfr  5298  ralxfrALT  5306  sspwb  5332  copsexgw  5372  copsexg  5373  snopeqop  5387  propeqop  5388  opthhausdorff  5398  opthhausdorff0  5399  pocl  5474  pofun  5484  solin  5491  frss  5515  2optocl  5639  3optocl  5640  ssrel  5650  ssrel2  5652  ssrelrel  5662  relop  5714  dfres3  5851  asymref2  5970  xpidtr  5975  trin2  5976  poltletr  5985  xp11  6025  relcnvtrg  6112  reuop  6137  tz7.7  6210  ordtr2  6228  suc11  6287  iotaval  6322  funmo  6364  fundif  6396  fss  6520  f0dom0  6556  fv3  6681  tz6.12i  6689  mpteqb  6779  fveqdmss  6838  eldmrexrnb  6850  funopsn  6902  funsndifnop  6905  tpres  6955  funfvima  6983  fvclss  6992  f1veqaeq  7006  isoselem  7083  oprabv  7203  ovg  7302  elovmpt3rab1  7394  sorpsscmpl  7449  iunpw  7482  ordom  7578  limom  7584  peano5  7594  fornex  7646  funelss  7735  funeldmdif  7736  bropopvvv  7774  bropfvvvvlem  7775  f1o2ndf1  7807  poxp  7811  soxp  7812  suppimacnv  7830  ressuppss  7838  ressuppssdif  7840  tposfn2  7903  wfr3g  7942  onnseq  7970  smoel  7986  smogt  7993  smoiso2  7995  tfr3  8024  tz7.48-2  8067  tz7.48-3  8069  tz7.49  8070  oecl  8151  oaordex  8173  oalimcl  8175  oaass  8176  omordi  8181  omlimcl  8193  odi  8194  omeulem1  8197  oen0  8201  nnawordi  8236  nnaass  8237  nnmordi  8246  omabs  8263  omsmolem  8269  iiner  8358  2ecoptocl  8377  3ecoptocl  8378  undifixp  8486  xpdom2  8600  xpf1o  8667  infensuc  8683  php  8689  onomeneq  8696  isinf  8719  findcard2  8746  unblem2  8759  infssuni  8803  finsschain  8819  fsuppunfi  8841  fsuppunbi  8842  marypha1  8886  hartogs  8996  card2on  9006  card2inf  9007  xpwdomg  9037  elirrv  9048  en3lp  9065  preleqg  9066  inf3lem1  9079  inf3lem2  9080  inf3lem3  9081  inf3lem5  9083  noinfep  9111  trcl  9158  tcel  9175  rankonidlem  9245  scottex  9302  djuunxp  9338  eldju2ndl  9341  updjud  9351  dif1card  9424  fodomnum  9471  cardaleph  9503  kmlem9  9572  kmlem13  9576  cflim2  9673  cfsmolem  9680  infpssrlem3  9715  isfin7-2  9806  fin1a2lem6  9815  fin1a2lem12  9821  domtriomlem  9852  axdc3lem4  9863  axdc4lem  9865  zorn2lem3  9908  zorn2lem4  9909  zorn2lem5  9910  zorn2lem7  9912  zornn0g  9915  axdclem2  9930  ondomon  9973  alephval2  9982  cfpwsdom  9994  wuncval2  10157  grupr  10207  gruiun  10209  ingru  10225  grothomex  10239  indpi  10317  nqereu  10339  prlem934  10443  reclem2pr  10458  mulgt0sr  10515  supsrlem  10521  dedekind  10791  lemul1a  11482  squeeze0  11531  peano5nni  11629  nnunb  11881  nn0lt2  12033  nn0le2is012  12034  fzind  12068  nn0ind-raph  12070  zindd  12071  eluzadd  12261  uzin  12266  nn01to3  12329  xnn0xadd0  12628  xmulasslem  12666  icoshft  12847  fzen  12912  uzsubsubfz  12917  elfz0ubfz0  12999  elfz0fzfz0  13000  fz0fzelfz0  13001  elfzmlbp  13006  elfzodifsumelfzo  13091  ssfzo12bi  13120  elfzonelfzo  13127  elfznelfzo  13130  injresinjlem  13145  injresinj  13146  modfzo0difsn  13299  modsumfzodifsn  13300  addmodlteq  13302  ssnn0fi  13341  fsuppmapnn0fiub0  13349  expcllem  13428  expeq0  13447  mulexp  13456  leexp2r  13526  bernneq  13578  facdiv  13635  hasheqf1oi  13700  hashnn0n0nn  13740  hashss  13758  hashgt12el  13771  hashgt12el2  13772  hashimarni  13790  hashle2pr  13823  pr2pwpr  13825  hashge2el2dif  13826  hashge2el2difr  13827  hashtpg  13831  hashge3el3dif  13832  exprelprel  13835  hash1to3  13837  fundmge2nop0  13838  fi1uzind  13843  ccatsymb  13924  swrdnd  14004  swrdnd2  14005  swrdnnn0nd  14006  swrdnd0  14007  pfxnd0  14038  swrdswrdlem  14054  swrdswrd  14055  pfxccatin12lem2a  14077  pfxccatin12lem1  14078  swrdccatin2  14079  pfxccatin12lem2  14081  pfxccatin12lem3  14082  pfxccat3  14084  swrdccat  14085  swrdccat3blem  14089  repsdf2  14128  repswswrd  14134  cshwidxmod  14153  cshwidx0  14156  cshf1  14160  cshweqrep  14171  cshw1  14172  cshwsexa  14174  2cshwcshw  14175  scshwfzeqfzo  14176  cshwcsh2id  14178  wwlktovfo  14310  relexpaddg  14400  iseraltlem2  15027  modfsummods  15136  clim2prod  15232  prodfn0  15238  prodfrec  15239  prodmo  15278  fprodabs  15316  binomfallfac  15383  fprodefsum  15436  dvdsaddre2b  15645  addmodlteqALT  15663  oddge22np1  15686  nn0enne  15716  nn0o1gt2  15720  sumeven  15726  sumodd  15727  dvdslegcd  15841  gcdneg  15858  dfgcd2  15882  rplpwr  15895  lcmf  15965  lcmftp  15968  lcmfunsnlem2lem1  15970  lcmfunsnlem2  15972  lcmfdvdsb  15975  coprmdvds1  15984  qredeq  15989  coprmprod  15993  coprmproddvdslem  15994  cncongr1  15999  cncongr2  16000  prm2orodd  16023  2mulprm  16025  nnnn0modprm0  16131  prm23lt5  16139  prm23ge5  16140  dvdsprmpweqnn  16209  dvdsprmpweqle  16210  oddprmdvds  16227  prmpwdvds  16228  prmreclem4  16243  ramcl  16353  prmgaplem6  16380  prmgaplem7  16381  prmgaplem8  16382  cshwshashlem1  16417  cshwshashlem2  16418  cshwshashlem3  16419  cshwrepswhash1  16424  setsn0fun  16508  setsstruct2  16509  imasleval  16802  mreiincl  16855  mreexexd  16907  inveq  17032  cicsym  17062  cictr  17063  initoid  17253  termoid  17254  initoeu2lem0  17261  initoeu2lem1  17262  initoeu2lem2  17263  initoeu2  17264  fthestrcsetc  17388  fthsetcestrc  17403  drsdirfi  17536  isnmgm  17844  sgrpass  17895  insubm  17971  mgm2nsgrplem3  18023  dfgrp3lem  18135  cyccom  18284  symg2bas  18455  symgfix2  18473  symgextf1  18478  gsmsymgrfix  18485  pmtrprfv3  18511  psgnunilem4  18554  efgi2  18780  0ringnnzr  19970  mpfrcl  20226  gsummoncoe1  20400  psgndiflemB  20672  psgndiflemA  20673  elfrlmbasn0  20835  lmictra  20917  mamufacex  20928  matecl  20962  dmatelnd  21033  dmatscmcl  21040  scmateALT  21049  scmatsgrp1  21059  scmatf1  21068  mavmulsolcl  21088  cramerimplem1  21220  cramerimplem2  21221  pmatcollpw3fi1  21324  mp2pm2mplem4  21345  pm2mpfo  21350  chmaidscmat  21384  fvmptnn04ifb  21387  chfacfscmul0  21394  chfacfpmmul0  21398  cayhamlem1  21402  cayhamlem3  21423  cayleyhamilton1  21428  fiinopn  21437  tgcl  21505  distop  21531  isclo2  21624  iscldtop  21631  ssnei2  21652  opnnei  21656  pnfnei  21756  mnfnei  21757  tgcnp  21789  cnpnei  21800  1stcelcls  21997  txcnpi  22144  cnmptcom  22214  fbfinnfr  22377  isfildlem  22393  snfil  22400  fbunfip  22405  fgcl  22414  elfm2  22484  fmco  22497  fbflim2  22513  cnpflf2  22536  flimfcls  22562  tmdgsum  22631  neibl  23038  tngngpim  23195  fgcfil  23801  caubl  23838  volsuplem  24083  ellimc3  24404  dvnadd  24453  dvnres  24455  cpnord  24459  dvnfre  24476  ply1divex  24657  cxpmul2  25199  zabsle1  25799  gausslemma2dlem1a  25868  gausslemma2dlem3  25871  lgsquad2lem2  25888  2lgs  25910  2sq2  25936  2sqnn0  25941  2sqnn  25942  2sqreultlem  25950  2sqreunnltlem  25953  qabvexp  26129  axcontlem4  26680  umgredgprv  26819  umgrnloop  26820  upgrpredgv  26851  upgredgpr  26854  edglnl  26855  usgredgprvALT  26904  usgrnloopALT  26912  usgredg2v  26936  fusgrfis  27039  nbuhgr2vtx1edgblem  27060  nb3grprlem1  27089  cusgrsize2inds  27162  cusgrfi  27167  fusgrn0degnn0  27208  uspgrloopvtxel  27225  vtxdginducedm1lem4  27251  uhgr0edg0rgrb  27283  wlkl1loop  27346  wlk1walk  27347  upgriswlk  27349  upgrwlkvtxedg  27353  uspgr2wlkeq  27354  wlkv0  27359  wlklenvclwlkOLD  27364  wlksoneq1eq2  27373  wlkon2n0  27375  wlkreslem  27378  wlkres  27379  lfgrwlkprop  27396  pthdivtx  27437  2pthnloop  27439  spthonepeq  27460  uhgrwkspthlem2  27462  uhgrwkspth  27463  usgr2wlkneq  27464  usgr2trlncl  27468  usgr2pthlem  27471  usgr2pth  27472  cyclnspth  27508  lfgrn1cycl  27510  usgr2trlncrct  27511  uspgrn2crct  27513  crctcshwlkn0lem3  27517  crctcshwlkn0lem5  27519  wwlknp  27548  wspthneq1eq2  27565  0enwwlksnge1  27569  wlklnwwlkln1  27573  wlkiswwlks2  27580  wlkiswwlksupgr2  27582  wlklnwwlkln2lem  27587  wwlksnred  27597  wwlksnextbi  27599  wwlksnredwwlkn0  27601  wwlksnextwrd  27602  wwlksnextinj  27604  wwlksnextproplem3  27617  wwlksnextprop  27618  wspthsnwspthsnon  27622  wspthsnonn0vne  27623  2pthon3v  27649  umgr2adedgwlkonALT  27653  umgr2wlk  27655  umgr2wlkon  27656  umgrwwlks2on  27663  elwspths2on  27666  usgr2wspthons3  27670  elwwlks2  27672  rusgrnumwwlk  27681  clwwlkccatlem  27694  clwlkclwwlklem2a4  27702  clwlkclwwlklem2a  27703  clwlkclwwlklem2  27705  clwlkclwwlkf1lem3  27711  erclwwlkeqlen  27724  clwwlknwwlksn  27743  loopclwwlkn1b  27747  clwwlkf1  27755  wwlksext2clwwlk  27763  eleclclwwlknlem2  27767  umgr2cwwk2dif  27770  eleclclwwlkn  27782  hashecclwwlkn1  27783  umgrhashecclwwlk  27784  clwwlknonwwlknonb  27812  clwwlknonex2lem2  27814  clwwlknonex2  27815  1pthon2v  27859  upgr3v3e3cycl  27886  uhgr3cyclexlem  27887  uhgr3cyclex  27888  eupth2lem3lem4  27937  frgr3vlem1  27979  frgr3vlem2  27980  3vfriswmgrlem  27983  3vfriswmgr  27984  3cyclfrgrrn1  27991  n4cyclfrgr  27997  frgrncvvdeqlem3  28007  frgrncvvdeqlem6  28010  frgrncvvdeqlem7  28011  frgrncvvdeqlem8  28012  frgrwopreglem4a  28016  frgrwopreglem3  28020  frgrwopreg1  28024  frgrwopreg2  28025  frgrwopreglem5lem  28026  frgrwopreglem5ALT  28028  frgrwopreg  28029  fusgr2wsp2nb  28040  2wspmdisj  28043  numclwwlk1lem2foa  28060  numclwwlk1lem2f1  28063  numclwwlk1lem2fo  28064  numclwwlk1  28067  wlkl0  28073  numclwwlk2lem1  28082  numclwlk2lem2f  28083  numclwlk2lem2f1o  28085  frgrreg  28100  frgrregord013  28101  frgrregord13  28102  friendshipgt3  28104  friendship  28105  eulplig  28189  ipassi  28545  ubthlem2  28575  isch3  28945  shintcli  29033  shmodsi  29093  spansncvi  29356  hoaddsub  29520  eigorthi  29541  pjss2coi  29868  pjnormssi  29872  pj3cor1i  29913  strb  29962  dmdmd  30004  mdsl0  30014  csmdsymi  30038  chrelat2i  30069  mdsymlem3  30109  mdsymlem6  30112  sumdmdlem2  30123  opreu2reuALT  30167  ssrelf  30294  spthcycl  32273  loop1cycl  32281  cvmlift2lem1  32446  satfrel  32511  satfrnmapom  32514  fmlafvel  32529  fmla1  32531  gonarlem  32538  gonar  32539  goalrlem  32540  goalr  32541  satffunlem  32545  satffunlem1lem1  32546  satffunlem2lem1  32548  satffun  32553  satefvfmla1  32569  mrsubvrs  32666  mclsax  32713  3ccased  32846  dfon2lem3  32927  rdgprc  32936  trpredmintr  32967  trpredrec  32974  frr3g  33018  sltval2  33060  nolt02o  33096  sslttr  33165  scutun12  33168  cgrextend  33366  btwndiff  33385  btwnconn1lem12  33456  brsegle  33466  broutsideof2  33480  funray  33498  elicc3  33562  nn0prpwlem  33567  nn0prpw  33568  fnessref  33602  neibastop2lem  33605  filnetlem4  33626  meran1  33656  waj-ax  33659  arg-ax  33661  bj-con2com  33793  bj-axdd2  33823  bj-alrimg  33849  bj-exlimg  33853  bj-exalimi  33863  bj-cbvalimt  33869  bj-eximcom  33873  bj-ssbid1ALT  33895  bj-sb  33918  bj-dtru  34036  bj-snsetex  34172  bj-restpw  34277  bj-finsumval0  34455  mptsnunlem  34501  icoreclin  34520  relowlpssretop  34527  inunissunidif  34538  rdgssun  34541  finorwe  34545  domalom  34567  wl-dral1d  34652  wl-exeq  34655  wl-lem-exsb  34683  poimirlem29  34802  poimirlem32  34805  fdc  34901  seqpo  34903  incsequz  34904  isismty  34960  ismtybndlem  34965  heibor1lem  34968  ismgmOLD  35009  isexid2  35014  ghomco  35050  pridlc  35230  relcnveq3  35459  elrelscnveq3  35611  cdleme18d  37311  tendovalco  37781  cdlemn11pre  38226  dihord2pre  38241  nnadddir  39041  incssnn0  39186  fphpd  39291  jm2.19lem3  39466  setindtr  39499  islssfg2  39549  mpaaeu  39628  pr2cv  39785  refimssco  39845  iunrelexpmin1  39931  iunrelexpmin2  39935  trclimalb2  39949  clsk1indlem3  40271  syldbl2  40397  tfindsd  40441  mnurndlem1  40494  nzss  40526  sb5ALT  40736  truniALT  40752  ee223  40845  3orbi123VD  41061  sbc3orgVD  41062  exbirVD  41064  exbiriVD  41065  sbcim2gVD  41086  trsbcVD  41088  truniALTVD  41089  onfrALTlem3VD  41098  onfrALTlem2VD  41100  csbrngVD  41107  19.41rgVD  41113  ax6e2eqVD  41118  ax6e2ndeqVD  41120  2uasbanhVD  41122  sb5ALTVD  41124  vk15.4jVD  41125  infxrunb3rnmpt  41578  stoweidlem26  42188  hirstL-ax3  43005  rexsb  43174  rexrsb  43175  euoreqb  43185  2reu8i  43189  afvres  43248  tz6.12-afv  43249  afvco2  43252  afv2orxorb  43304  afv2res  43315  tz6.12-afv2  43316  tz6.12i-afv2  43319  dfatcolem  43331  zm1nn  43379  fzoopth  43404  2ffzoeq  43405  smonoord  43408  iccpartiltu  43459  iccpartlt  43461  iccpartltu  43462  iccpartgtl  43463  iccpartgt  43464  iccpartleu  43465  iccpartgel  43466  icceuelpart  43473  iccpartnel  43475  lswn0  43481  ichnreuop  43511  ichreuopeq  43512  prsprel  43526  sprsymrelfvlem  43529  sprsymrelf1lem  43530  sprsymrelfolem2  43532  prproropf1olem4  43545  paireqne  43550  prprelb  43555  reupr  43561  goldbachth  43586  odz2prm2pw  43602  fmtno4prmfac  43611  fmtno4prmfac193  43612  prmdvdsfmtnof1lem2  43624  2pwp1prmfmtno  43629  lighneallem2  43648  lighneallem4b  43651  lighneallem4  43652  requad2  43665  odd2prm2  43760  mogoldbblem  43762  gbepos  43800  gbowgt5  43804  gbowge7  43805  stgoldbwt  43818  sbgoldbwt  43819  sbgoldbst  43820  sbgoldbaltlem1  43821  sbgoldbalt  43823  sbgoldbo  43829  nnsum3primesle9  43836  nnsum4primesodd  43838  nnsum4primesoddALTV  43839  nnsum4primeseven  43842  nnsum4primesevenALTV  43843  bgoldbtbndlem1  43847  bgoldbtbndlem2  43848  bgoldbtbndlem3  43849  bgoldbtbnd  43851  isomuspgrlem1  43869  upgrwlkupwlk  43892  uspgrsprf1  43899  mgmhmlin  43930  issubmgm2  43934  lmod0rng  44067  lidldomn1  44120  lidlmmgm  44124  rnghmsscmap  44173  rnghmsubcsetclem2  44175  rngcinv  44180  rngccatidALTV  44188  rngcinvALTV  44192  funcrngcsetc  44197  funcrngcsetcALT  44198  rhmsscmap  44219  rhmsubcsetclem2  44221  rhmsubcrngclem2  44227  ringcinv  44231  ringcbasbas  44233  funcringcsetc  44234  funcringcsetcALTV2lem9  44243  ringccatidALTV  44251  ringcinvALTV  44255  ringcbasbasALTV  44257  rhmsubclem4  44288  rhmsubcALTVlem4  44306  ztprmneprm  44323  pgrpgt2nabl  44342  lmodvsmdi  44358  ply1mulgsumlem2  44369  lincsumcl  44414  ellcoellss  44418  linindslinci  44431  islinindfis  44432  lincext3  44439  lindslinindimp2lem4  44444  lindslinindsimp2lem5  44445  lindslinindsimp2  44446  lindsrng01  44451  ldepspr  44456  lincresunit3lem1  44462  elfzolborelfzop1  44502  dignn0ldlem  44590  nn0sumshdiglem1  44609  rrx2xpref1o  44633  rrx2plord2  44637  rrx2plordisom  44638  line2ylem  44666  line2xlem  44668  line2y  44670  itschlc0xyqsol1  44681  inlinecirc02plem  44701  tfis2d  44711  onsetrec  44738
  Copyright terms: Public domain W3C validator