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  179  jad  189  pm2.61  194  syl5ibcom  247  syl5ibrcom  249  pm5.501  369  impcom  410  impd  413  expcom  416  expdcom  417  simplbi2com  505  imdistanri  572  jaod  855  orel1  885  pm2.62  896  pm2.75  930  pm2.64  938  ccased  1033  dedlem0b  1039  3impd  1344  3expd  1349  mp3an1i  1450  norassOLD  1534  minimp  1622  meredith  1642  19.35  1878  speimfw  1966  equtrr  2029  equeucl  2031  sb56OLD  2278  sbiedw  2332  sbiedwOLD  2333  cbv1v  2356  exsb  2378  cbv1  2422  ax12b  2446  axc11n  2448  dvelimdf  2471  equvel  2479  dfsb1  2510  sbequ2OLDOLD  2514  sbied  2545  sbequ2ALT  2580  sbiedALT  2614  dfmoeu  2618  mo3  2647  mo4  2649  2mo  2732  2eu6  2741  exists2  2746  rexlimdv  3270  r19.12  3311  r19.12OLD  3314  r19.35  3328  2gencl  3514  3gencl  3515  vtocl2ga  3554  rspccv  3599  ceqex  3624  mob  3688  euind  3695  reuind  3724  2reu1  3858  sseq2  3972  nelss  4009  rexdifi  4101  reupick2  4267  rspn0  4289  disjeq0  4381  uneqdifeq  4414  sspw  4528  ssprsseq  4734  preq12b  4757  prnebg  4762  prel12g  4770  3elpr2eq  4813  iinss2  4957  trintss  5165  dtru  5247  reusv2lem1  5275  alxfr  5284  ralxfrALT  5292  copsexgw  5357  copsexg  5358  snopeqop  5372  propeqop  5373  opthhausdorff  5383  opthhausdorff0  5384  pocl  5457  pofun  5467  solin  5474  frss  5498  2optocl  5622  3optocl  5623  ssrel  5633  ssrel2  5635  ssrelrel  5645  relop  5697  dfres3  5834  asymref2  5953  xpidtr  5958  trin2  5959  poltletr  5968  xp11  6008  relcnvtrg  6095  reuop  6120  tz7.7  6193  ordtr2  6211  suc11  6270  iotaval  6305  funmo  6347  fundif  6379  fss  6503  f0dom0  6539  fv3  6664  tz6.12i  6672  mpteqb  6763  fveqdmss  6822  eldmrexrnb  6834  funopsn  6886  funsndifnop  6889  tpres  6939  funfvima  6969  fvclss  6978  f1veqaeq  6992  isoselem  7071  oprabv  7191  ovg  7291  elovmpt3rab1  7383  sorpsscmpl  7438  iunpw  7471  ordom  7567  limom  7573  peano5  7583  fornex  7635  funelss  7724  funeldmdif  7725  bropopvvv  7763  bropfvvvvlem  7764  f1o2ndf1  7796  poxp  7800  soxp  7801  suppimacnv  7819  ressuppss  7827  ressuppssdif  7829  tposfn2  7892  wfr3g  7931  onnseq  7959  smoel  7975  smogt  7982  smoiso2  7984  tfr3  8013  tz7.48-2  8056  tz7.48-3  8058  tz7.49  8059  oecl  8140  oaordex  8162  oalimcl  8164  oaass  8165  omordi  8170  omlimcl  8182  odi  8183  omeulem1  8186  oen0  8190  nnawordi  8225  nnaass  8226  nnmordi  8235  omabs  8252  omsmolem  8258  iiner  8347  2ecoptocl  8366  3ecoptocl  8367  undifixp  8476  xpdom2  8590  xpf1o  8657  infensuc  8673  php  8679  onomeneq  8686  isinf  8709  findcard2  8736  unblem2  8749  infssuni  8793  finsschain  8809  fsuppunfi  8831  fsuppunbi  8832  marypha1  8876  hartogs  8986  card2on  8996  card2inf  8997  xpwdomg  9027  elirrv  9038  en3lp  9055  preleqg  9056  inf3lem1  9069  inf3lem2  9070  inf3lem3  9071  inf3lem5  9073  noinfep  9101  trcl  9148  tcel  9165  rankonidlem  9235  scottex  9292  djuunxp  9328  eldju2ndl  9331  updjud  9341  dif1card  9414  fodomnum  9461  cardaleph  9493  kmlem9  9562  kmlem13  9566  cflim2  9663  cfsmolem  9670  infpssrlem3  9705  isfin7-2  9796  fin1a2lem6  9805  fin1a2lem12  9811  domtriomlem  9842  axdc3lem4  9853  axdc4lem  9855  zorn2lem3  9898  zorn2lem4  9899  zorn2lem5  9900  zorn2lem7  9902  zornn0g  9905  axdclem2  9920  ondomon  9963  alephval2  9972  cfpwsdom  9984  wuncval2  10147  grupr  10197  gruiun  10199  ingru  10215  grothomex  10229  indpi  10307  nqereu  10329  prlem934  10433  reclem2pr  10448  mulgt0sr  10505  supsrlem  10511  dedekind  10781  lemul1a  11472  squeeze0  11521  peano5nni  11619  nnunb  11872  nn0lt2  12024  nn0le2is012  12025  fzind  12059  nn0ind-raph  12061  zindd  12062  eluzadd  12252  uzin  12257  nn01to3  12320  xnn0xadd0  12619  xmulasslem  12657  icoshft  12842  fzen  12908  uzsubsubfz  12913  elfz0ubfz0  12995  elfz0fzfz0  12996  fz0fzelfz0  12997  elfzmlbp  13002  elfzodifsumelfzo  13087  ssfzo12bi  13116  elfzonelfzo  13123  elfznelfzo  13126  injresinjlem  13141  injresinj  13142  modfzo0difsn  13295  modsumfzodifsn  13296  addmodlteq  13298  ssnn0fi  13337  fsuppmapnn0fiub0  13345  expcllem  13425  expeq0  13444  mulexp  13453  leexp2r  13523  bernneq  13575  facdiv  13632  hasheqf1oi  13697  hashnn0n0nn  13737  hashss  13755  hashgt12el  13768  hashgt12el2  13769  hashimarni  13787  hashle2pr  13820  pr2pwpr  13822  hashge2el2dif  13823  hashge2el2difr  13824  hashtpg  13828  hashge3el3dif  13829  exprelprel  13832  hash1to3  13834  fundmge2nop0  13835  fi1uzind  13840  ccatsymb  13916  swrdnd  13996  swrdnd2  13997  swrdnnn0nd  13998  swrdnd0  13999  pfxnd0  14030  swrdswrdlem  14046  swrdswrd  14047  pfxccatin12lem2a  14069  pfxccatin12lem1  14070  swrdccatin2  14071  pfxccatin12lem2  14073  pfxccatin12lem3  14074  pfxccat3  14076  swrdccat  14077  swrdccat3blem  14081  repsdf2  14120  repswswrd  14126  cshwidxmod  14145  cshwidx0  14148  cshf1  14152  cshweqrep  14163  cshw1  14164  cshwsexa  14166  2cshwcshw  14167  scshwfzeqfzo  14168  cshwcsh2id  14170  wwlktovfo  14302  relexpaddg  14392  iseraltlem2  15019  modfsummods  15128  clim2prod  15224  prodfn0  15230  prodfrec  15231  prodmo  15270  fprodabs  15308  binomfallfac  15375  fprodefsum  15428  dvdsaddre2b  15637  addmodlteqALT  15655  oddge22np1  15678  nn0enne  15706  nn0o1gt2  15710  sumeven  15716  sumodd  15717  dvdslegcd  15831  gcdneg  15848  dfgcd2  15872  rplpwr  15885  lcmf  15955  lcmftp  15958  lcmfunsnlem2lem1  15960  lcmfunsnlem2  15962  lcmfdvdsb  15965  coprmdvds1  15974  qredeq  15979  coprmprod  15983  coprmproddvdslem  15984  cncongr1  15989  cncongr2  15990  prm2orodd  16013  2mulprm  16015  nnnn0modprm0  16121  prm23lt5  16129  prm23ge5  16130  dvdsprmpweqnn  16199  dvdsprmpweqle  16200  oddprmdvds  16217  prmpwdvds  16218  prmreclem4  16233  ramcl  16343  prmgaplem6  16370  prmgaplem7  16371  prmgaplem8  16372  cshwshashlem1  16408  cshwshashlem2  16409  cshwshashlem3  16410  cshwrepswhash1  16415  setsn0fun  16499  setsstruct2  16500  imasleval  16793  mreiincl  16846  mreexexd  16898  inveq  17023  cicsym  17053  cictr  17054  initoid  17244  termoid  17245  initoeu2lem0  17252  initoeu2lem1  17253  initoeu2lem2  17254  initoeu2  17255  fthestrcsetc  17379  fthsetcestrc  17394  drsdirfi  17527  isnmgm  17835  sgrpass  17886  insubm  17962  mgm2nsgrplem3  18064  dfgrp3lem  18176  cyccom  18325  symg2bas  18500  symgfix2  18523  symgextf1  18528  gsmsymgrfix  18535  pmtrprfv3  18561  psgnunilem4  18604  efgi2  18830  0ringnnzr  20018  mpfrcl  20274  gsummoncoe1  20448  psgndiflemB  20720  psgndiflemA  20721  elfrlmbasn0  20883  lmictra  20965  mamufacex  20976  matecl  21010  dmatelnd  21081  dmatscmcl  21088  scmateALT  21097  scmatsgrp1  21107  scmatf1  21116  mavmulsolcl  21136  cramerimplem1  21268  cramerimplem2  21269  pmatcollpw3fi1  21372  mp2pm2mplem4  21393  pm2mpfo  21398  chmaidscmat  21432  fvmptnn04ifb  21435  chfacfscmul0  21442  chfacfpmmul0  21446  cayhamlem1  21450  cayhamlem3  21471  cayleyhamilton1  21476  fiinopn  21485  tgcl  21553  distop  21579  isclo2  21672  iscldtop  21679  ssnei2  21700  opnnei  21704  pnfnei  21804  mnfnei  21805  tgcnp  21837  cnpnei  21848  1stcelcls  22045  txcnpi  22192  cnmptcom  22262  fbfinnfr  22425  isfildlem  22441  snfil  22448  fbunfip  22453  fgcl  22462  elfm2  22532  fmco  22545  fbflim2  22561  cnpflf2  22584  flimfcls  22610  tmdgsum  22679  neibl  23087  tngngpim  23244  fgcfil  23854  caubl  23891  volsuplem  24138  ellimc3  24461  dvnadd  24511  dvnres  24513  cpnord  24517  dvnfre  24534  ply1divex  24716  cxpmul2  25259  zabsle1  25859  gausslemma2dlem1a  25928  gausslemma2dlem3  25931  lgsquad2lem2  25948  2lgs  25970  2sq2  25996  2sqnn0  26001  2sqnn  26002  2sqreultlem  26010  2sqreunnltlem  26013  qabvexp  26189  axcontlem4  26740  umgredgprv  26879  umgrnloop  26880  upgrpredgv  26911  upgredgpr  26914  edglnl  26915  usgredgprvALT  26964  usgrnloopALT  26972  usgredg2v  26996  fusgrfis  27099  nbuhgr2vtx1edgblem  27120  nb3grprlem1  27149  cusgrsize2inds  27222  cusgrfi  27227  fusgrn0degnn0  27268  uspgrloopvtxel  27285  vtxdginducedm1lem4  27311  uhgr0edg0rgrb  27343  wlkl1loop  27406  wlk1walk  27407  upgriswlk  27409  upgrwlkvtxedg  27413  uspgr2wlkeq  27414  wlkv0  27419  wlklenvclwlkOLD  27424  wlksoneq1eq2  27433  wlkon2n0  27435  wlkreslem  27438  wlkres  27439  lfgrwlkprop  27456  pthdivtx  27497  2pthnloop  27499  spthonepeq  27520  uhgrwkspthlem2  27522  uhgrwkspth  27523  usgr2wlkneq  27524  usgr2trlncl  27528  usgr2pthlem  27531  usgr2pth  27532  cyclnspth  27568  lfgrn1cycl  27570  usgr2trlncrct  27571  uspgrn2crct  27573  crctcshwlkn0lem3  27577  crctcshwlkn0lem5  27579  wwlknp  27608  wspthneq1eq2  27625  0enwwlksnge1  27629  wlklnwwlkln1  27633  wlkiswwlks2  27640  wlkiswwlksupgr2  27642  wlklnwwlkln2lem  27647  wwlksnred  27657  wwlksnextbi  27659  wwlksnredwwlkn0  27661  wwlksnextwrd  27662  wwlksnextinj  27664  wwlksnextproplem3  27676  wwlksnextprop  27677  wspthsnwspthsnon  27681  wspthsnonn0vne  27682  2pthon3v  27708  umgr2adedgwlkonALT  27712  umgr2wlk  27714  umgr2wlkon  27715  umgrwwlks2on  27722  elwspths2on  27725  usgr2wspthons3  27729  elwwlks2  27731  rusgrnumwwlk  27740  clwwlkccatlem  27753  clwlkclwwlklem2a4  27761  clwlkclwwlklem2a  27762  clwlkclwwlklem2  27764  clwlkclwwlkf1lem3  27770  erclwwlkeqlen  27783  clwwlknwwlksn  27802  loopclwwlkn1b  27806  clwwlkf1  27813  wwlksext2clwwlk  27821  eleclclwwlknlem2  27825  umgr2cwwk2dif  27828  eleclclwwlkn  27840  hashecclwwlkn1  27841  umgrhashecclwwlk  27842  clwwlknonwwlknonb  27870  clwwlknonex2lem2  27872  clwwlknonex2  27873  1pthon2v  27917  upgr3v3e3cycl  27944  uhgr3cyclexlem  27945  uhgr3cyclex  27946  eupth2lem3lem4  27995  frgr3vlem1  28037  frgr3vlem2  28038  3vfriswmgrlem  28041  3vfriswmgr  28042  3cyclfrgrrn1  28049  n4cyclfrgr  28055  frgrncvvdeqlem3  28065  frgrncvvdeqlem6  28068  frgrncvvdeqlem7  28069  frgrncvvdeqlem8  28070  frgrwopreglem4a  28074  frgrwopreglem3  28078  frgrwopreg1  28082  frgrwopreg2  28083  frgrwopreglem5lem  28084  frgrwopreglem5ALT  28086  frgrwopreg  28087  fusgr2wsp2nb  28098  2wspmdisj  28101  numclwwlk1lem2foa  28118  numclwwlk1lem2f1  28121  numclwwlk1lem2fo  28122  numclwwlk1  28125  wlkl0  28131  numclwwlk2lem1  28140  numclwlk2lem2f  28141  numclwlk2lem2f1o  28143  frgrreg  28158  frgrregord013  28159  frgrregord13  28160  friendshipgt3  28162  friendship  28163  eulplig  28247  ipassi  28603  ubthlem2  28633  isch3  29003  shintcli  29091  shmodsi  29151  spansncvi  29414  hoaddsub  29578  eigorthi  29599  pjss2coi  29926  pjnormssi  29930  pj3cor1i  29971  strb  30020  dmdmd  30062  mdsl0  30072  csmdsymi  30096  chrelat2i  30127  mdsymlem3  30167  mdsymlem6  30170  sumdmdlem2  30181  opreu2reuALT  30225  ssrelf  30353  spthcycl  32384  loop1cycl  32392  cvmlift2lem1  32557  satfrel  32622  satfrnmapom  32625  fmlafvel  32640  fmla1  32642  gonarlem  32649  gonar  32650  goalrlem  32651  goalr  32652  satffunlem  32656  satffunlem1lem1  32657  satffunlem2lem1  32659  satffun  32664  satefvfmla1  32680  mrsubvrs  32777  mclsax  32824  3ccased  32957  dfon2lem3  33038  rdgprc  33047  trpredmintr  33078  trpredrec  33085  frr3g  33129  sltval2  33171  nolt02o  33207  sslttr  33276  scutun12  33279  cgrextend  33477  btwndiff  33496  btwnconn1lem12  33567  brsegle  33577  broutsideof2  33591  funray  33609  elicc3  33673  nn0prpwlem  33678  nn0prpw  33679  fnessref  33713  neibastop2lem  33716  filnetlem4  33737  meran1  33767  waj-ax  33770  arg-ax  33772  bj-con2com  33904  bj-axdd2  33934  bj-alrimg  33960  bj-exlimg  33964  bj-exalimi  33974  bj-cbvalimt  33980  bj-eximcom  33984  bj-ssbid1ALT  34006  bj-sb  34029  bj-dtru  34147  bj-snsetex  34292  bj-restpw  34400  bj-finsumval0  34584  mptsnunlem  34636  icoreclin  34655  relowlpssretop  34662  inunissunidif  34673  rdgssun  34676  finorwe  34680  domalom  34702  wl-dral1d  34812  wl-exeq  34815  wl-lem-exsb  34843  poimirlem29  34962  poimirlem32  34965  fdc  35059  seqpo  35061  incsequz  35062  isismty  35115  ismtybndlem  35120  heibor1lem  35123  ismgmOLD  35164  isexid2  35169  ghomco  35205  pridlc  35385  relcnveq3  35614  elrelscnveq3  35767  cdleme18d  37467  tendovalco  37937  cdlemn11pre  38382  dihord2pre  38397  nnadddir  39283  incssnn0  39445  fphpd  39550  jm2.19lem3  39725  setindtr  39758  islssfg2  39808  mpaaeu  39887  pr2cv  40042  refimssco  40102  iunrelexpmin1  40188  iunrelexpmin2  40192  trclimalb2  40206  clsk1indlem3  40528  syldbl2  40654  tfindsd  40701  mnurndlem1  40772  nzss  40804  sb5ALT  41014  truniALT  41030  ee223  41123  3orbi123VD  41339  sbc3orgVD  41340  exbirVD  41342  exbiriVD  41343  sbcim2gVD  41364  trsbcVD  41366  truniALTVD  41367  onfrALTlem3VD  41376  onfrALTlem2VD  41378  csbrngVD  41385  19.41rgVD  41391  ax6e2eqVD  41396  ax6e2ndeqVD  41398  2uasbanhVD  41400  sb5ALTVD  41402  vk15.4jVD  41403  infxrunb3rnmpt  41856  stoweidlem26  42459  hirstL-ax3  43276  rexsb  43445  rexrsb  43446  euoreqb  43456  2reu8i  43460  afvres  43519  tz6.12-afv  43520  afvco2  43523  afv2orxorb  43575  afv2res  43586  tz6.12-afv2  43587  tz6.12i-afv2  43590  dfatcolem  43602  zm1nn  43650  fzoopth  43675  2ffzoeq  43676  smonoord  43679  iccpartiltu  43730  iccpartlt  43732  iccpartltu  43733  iccpartgtl  43734  iccpartgt  43735  iccpartleu  43736  iccpartgel  43737  icceuelpart  43744  iccpartnel  43746  lswn0  43752  ichnreuop  43780  ichreuopeq  43781  prsprel  43795  sprsymrelfvlem  43798  sprsymrelf1lem  43799  sprsymrelfolem2  43801  prproropf1olem4  43814  paireqne  43819  prprelb  43824  reupr  43830  goldbachth  43855  odz2prm2pw  43871  fmtno4prmfac  43880  fmtno4prmfac193  43881  prmdvdsfmtnof1lem2  43893  2pwp1prmfmtno  43898  lighneallem2  43916  lighneallem4b  43919  lighneallem4  43920  requad2  43933  odd2prm2  44028  mogoldbblem  44030  gbepos  44068  gbowgt5  44072  gbowge7  44073  stgoldbwt  44086  sbgoldbwt  44087  sbgoldbst  44088  sbgoldbaltlem1  44089  sbgoldbalt  44091  sbgoldbo  44097  nnsum3primesle9  44104  nnsum4primesodd  44106  nnsum4primesoddALTV  44107  nnsum4primeseven  44110  nnsum4primesevenALTV  44111  bgoldbtbndlem1  44115  bgoldbtbndlem2  44116  bgoldbtbndlem3  44117  bgoldbtbnd  44119  isomuspgrlem1  44137  upgrwlkupwlk  44160  uspgrsprf1  44167  mgmhmlin  44198  issubmgm2  44202  lmod0rng  44284  lidldomn1  44337  lidlmmgm  44341  rnghmsscmap  44390  rnghmsubcsetclem2  44392  rngcinv  44397  rngccatidALTV  44405  rngcinvALTV  44409  funcrngcsetc  44414  funcrngcsetcALT  44415  rhmsscmap  44436  rhmsubcsetclem2  44438  rhmsubcrngclem2  44444  ringcinv  44448  ringcbasbas  44450  funcringcsetc  44451  funcringcsetcALTV2lem9  44460  ringccatidALTV  44468  ringcinvALTV  44472  ringcbasbasALTV  44474  rhmsubclem4  44505  rhmsubcALTVlem4  44523  ztprmneprm  44540  pgrpgt2nabl  44559  lmodvsmdi  44575  ply1mulgsumlem2  44586  lincsumcl  44631  ellcoellss  44635  linindslinci  44648  islinindfis  44649  lincext3  44656  lindslinindimp2lem4  44661  lindslinindsimp2lem5  44662  lindslinindsimp2  44663  lindsrng01  44668  ldepspr  44673  lincresunit3lem1  44679  elfzolborelfzop1  44719  dignn0ldlem  44807  nn0sumshdiglem1  44826  rrx2xpref1o  44892  rrx2plord2  44896  rrx2plordisom  44897  line2ylem  44925  line2xlem  44927  line2y  44929  itschlc0xyqsol1  44940  inlinecirc02plem  44960  tfis2d  44970  onsetrec  44997
  Copyright terms: Public domain W3C validator