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  2270  sbiedw  2324  sbiedwOLD  2325  cbv1v  2348  exsb  2371  cbv1  2416  ax12b  2441  axc11n  2443  dvelimdf  2466  equvel  2474  dfsb1  2506  sbequ2OLDOLD  2510  sbied  2541  sbequ2ALT  2576  sbiedALT  2610  dfmoeu  2614  mo3  2644  mo4  2646  2mo  2729  2eu6  2740  exists2  2745  rexlimdv  3283  r19.12  3324  r19.12OLD  3327  r19.35  3341  2gencl  3536  3gencl  3537  vtocl2ga  3575  rspccv  3619  ceqex  3644  mob  3707  euind  3714  reuind  3743  2reu1  3880  sseq2  3992  nelss  4029  rexdifi  4121  reupick2  4288  rspn0  4312  disjeq0  4403  uneqdifeq  4436  ssprsseq  4752  preq12b  4775  prnebg  4780  prel12g  4788  3elpr2eq  4831  iinss2  4973  trintss  5181  dtru  5263  reusv2lem1  5290  alxfr  5299  ralxfrALT  5307  sspwb  5333  copsexgw  5373  copsexg  5374  snopeqop  5388  propeqop  5389  opthhausdorff  5399  opthhausdorff0  5400  pocl  5475  pofun  5485  solin  5492  frss  5516  2optocl  5640  3optocl  5641  ssrel  5651  ssrel2  5653  ssrelrel  5663  relop  5715  dfres3  5852  asymref2  5971  xpidtr  5976  trin2  5977  poltletr  5986  xp11  6026  relcnvtrg  6113  reuop  6138  tz7.7  6211  ordtr2  6229  suc11  6288  iotaval  6323  funmo  6365  fundif  6397  fss  6521  f0dom0  6557  fv3  6682  tz6.12i  6690  mpteqb  6780  fveqdmss  6839  eldmrexrnb  6851  funopsn  6903  funsndifnop  6906  tpres  6956  funfvima  6984  fvclss  6992  f1veqaeq  7006  isoselem  7083  oprabv  7203  ovg  7302  elovmpt3rab1  7394  sorpsscmpl  7449  iunpw  7481  ordom  7577  limom  7583  peano5  7593  fornex  7648  funelss  7737  funeldmdif  7738  bropopvvv  7776  bropfvvvvlem  7777  f1o2ndf1  7809  poxp  7813  soxp  7814  suppimacnv  7832  ressuppss  7840  ressuppssdif  7842  tposfn2  7905  wfr3g  7944  onnseq  7972  smoel  7988  smogt  7995  smoiso2  7997  tfr3  8026  tz7.48-2  8069  tz7.48-3  8071  tz7.49  8072  oecl  8153  oaordex  8174  oalimcl  8176  oaass  8177  omordi  8182  omlimcl  8194  odi  8195  omeulem1  8198  oen0  8202  nnawordi  8237  nnaass  8238  nnmordi  8247  omabs  8264  omsmolem  8270  iiner  8359  2ecoptocl  8378  3ecoptocl  8379  undifixp  8487  xpdom2  8601  xpf1o  8668  infensuc  8684  php  8690  onomeneq  8697  isinf  8720  findcard2  8747  unblem2  8760  infssuni  8804  finsschain  8820  fsuppunfi  8842  fsuppunbi  8843  marypha1  8887  hartogs  8997  card2on  9007  card2inf  9008  xpwdomg  9038  elirrv  9049  en3lp  9066  preleqg  9067  inf3lem1  9080  inf3lem2  9081  inf3lem3  9082  inf3lem5  9084  noinfep  9112  trcl  9159  tcel  9176  rankonidlem  9246  scottex  9303  djuunxp  9339  eldju2ndl  9342  updjud  9352  dif1card  9425  fodomnum  9472  cardaleph  9504  kmlem9  9573  kmlem13  9577  cflim2  9674  cfsmolem  9681  infpssrlem3  9716  isfin7-2  9807  fin1a2lem6  9816  fin1a2lem12  9822  domtriomlem  9853  axdc3lem4  9864  axdc4lem  9866  zorn2lem3  9909  zorn2lem4  9910  zorn2lem5  9911  zorn2lem7  9913  zornn0g  9916  axdclem2  9931  ondomon  9974  alephval2  9983  cfpwsdom  9995  wuncval2  10158  grupr  10208  gruiun  10210  ingru  10226  grothomex  10240  indpi  10318  nqereu  10340  prlem934  10444  reclem2pr  10459  mulgt0sr  10516  supsrlem  10522  dedekind  10792  lemul1a  11483  squeeze0  11532  peano5nni  11630  nnunb  11882  nn0lt2  12034  nn0le2is012  12035  fzind  12069  nn0ind-raph  12071  zindd  12072  eluzadd  12262  uzin  12267  nn01to3  12330  xnn0xadd0  12630  xmulasslem  12668  icoshft  12849  fzen  12914  uzsubsubfz  12919  elfz0ubfz0  13001  elfz0fzfz0  13002  fz0fzelfz0  13003  elfzmlbp  13008  elfzodifsumelfzo  13093  ssfzo12bi  13122  elfzonelfzo  13129  elfznelfzo  13132  injresinjlem  13147  injresinj  13148  modfzo0difsn  13301  modsumfzodifsn  13302  addmodlteq  13304  ssnn0fi  13343  fsuppmapnn0fiub0  13351  expcllem  13430  expeq0  13449  mulexp  13458  leexp2r  13528  bernneq  13580  facdiv  13637  hasheqf1oi  13702  hashnn0n0nn  13742  hashss  13760  hashgt12el  13773  hashgt12el2  13774  hashimarni  13792  hashle2pr  13825  pr2pwpr  13827  hashge2el2dif  13828  hashge2el2difr  13829  hashtpg  13833  hashge3el3dif  13834  exprelprel  13837  hash1to3  13839  fundmge2nop0  13840  fi1uzind  13845  ccatsymb  13926  swrdnd  14006  swrdnd2  14007  swrdnnn0nd  14008  swrdnd0  14009  pfxnd0  14040  swrdswrdlem  14056  swrdswrd  14057  pfxccatin12lem2a  14079  pfxccatin12lem1  14080  swrdccatin2  14081  pfxccatin12lem2  14083  pfxccatin12lem3  14084  pfxccat3  14086  swrdccat  14087  swrdccat3blem  14091  repsdf2  14130  repswswrd  14136  cshwidxmod  14155  cshwidx0  14158  cshf1  14162  cshweqrep  14173  cshw1  14174  cshwsexa  14176  2cshwcshw  14177  scshwfzeqfzo  14178  cshwcsh2id  14180  wwlktovfo  14312  relexpaddg  14402  iseraltlem2  15029  modfsummods  15138  clim2prod  15234  prodfn0  15240  prodfrec  15241  prodmo  15280  fprodabs  15318  binomfallfac  15385  fprodefsum  15438  dvdsaddre2b  15647  addmodlteqALT  15665  oddge22np1  15688  nn0enne  15718  nn0o1gt2  15722  sumeven  15728  sumodd  15729  dvdslegcd  15843  gcdneg  15860  dfgcd2  15884  rplpwr  15897  lcmf  15967  lcmftp  15970  lcmfunsnlem2lem1  15972  lcmfunsnlem2  15974  lcmfdvdsb  15977  coprmdvds1  15986  qredeq  15991  coprmprod  15995  coprmproddvdslem  15996  cncongr1  16001  cncongr2  16002  prm2orodd  16025  2mulprm  16027  nnnn0modprm0  16133  prm23lt5  16141  prm23ge5  16142  dvdsprmpweqnn  16211  dvdsprmpweqle  16212  oddprmdvds  16229  prmpwdvds  16230  prmreclem4  16245  ramcl  16355  prmgaplem6  16382  prmgaplem7  16383  prmgaplem8  16384  cshwshashlem1  16419  cshwshashlem2  16420  cshwshashlem3  16421  cshwrepswhash1  16426  setsn0fun  16510  setsstruct2  16511  imasleval  16804  mreiincl  16857  mreexexd  16909  inveq  17034  cicsym  17064  cictr  17065  initoid  17255  termoid  17256  initoeu2lem0  17263  initoeu2lem1  17264  initoeu2lem2  17265  initoeu2  17266  fthestrcsetc  17390  fthsetcestrc  17405  drsdirfi  17538  isnmgm  17846  sgrpass  17897  insubm  17973  mgm2nsgrplem3  18025  dfgrp3lem  18137  cyccom  18286  symg2bas  18457  symgfix2  18475  symgextf1  18480  gsmsymgrfix  18487  pmtrprfv3  18513  psgnunilem4  18556  efgi2  18782  0ringnnzr  19972  mpfrcl  20228  gsummoncoe1  20402  psgndiflemB  20674  psgndiflemA  20675  elfrlmbasn0  20837  lmictra  20919  mamufacex  20930  matecl  20964  dmatelnd  21035  dmatscmcl  21042  scmateALT  21051  scmatsgrp1  21061  scmatf1  21070  mavmulsolcl  21090  cramerimplem1  21222  cramerimplem2  21223  pmatcollpw3fi1  21326  mp2pm2mplem4  21347  pm2mpfo  21352  chmaidscmat  21386  fvmptnn04ifb  21389  chfacfscmul0  21396  chfacfpmmul0  21400  cayhamlem1  21404  cayhamlem3  21425  cayleyhamilton1  21430  fiinopn  21439  tgcl  21507  distop  21533  isclo2  21626  iscldtop  21633  ssnei2  21654  opnnei  21658  pnfnei  21758  mnfnei  21759  tgcnp  21791  cnpnei  21802  1stcelcls  21999  txcnpi  22146  cnmptcom  22216  fbfinnfr  22379  isfildlem  22395  snfil  22402  fbunfip  22407  fgcl  22416  elfm2  22486  fmco  22499  fbflim2  22515  cnpflf2  22538  flimfcls  22564  tmdgsum  22633  neibl  23040  tngngpim  23197  fgcfil  23803  caubl  23840  volsuplem  24085  ellimc3  24406  dvnadd  24455  dvnres  24457  cpnord  24461  dvnfre  24478  ply1divex  24659  cxpmul2  25199  zabsle1  25800  gausslemma2dlem1a  25869  gausslemma2dlem3  25872  lgsquad2lem2  25889  2lgs  25911  2sq2  25937  2sqnn0  25942  2sqnn  25943  2sqreultlem  25951  2sqreunnltlem  25954  qabvexp  26130  axcontlem4  26681  umgredgprv  26820  umgrnloop  26821  upgrpredgv  26852  upgredgpr  26855  edglnl  26856  usgredgprvALT  26905  usgrnloopALT  26913  usgredg2v  26937  fusgrfis  27040  nbuhgr2vtx1edgblem  27061  nb3grprlem1  27090  cusgrsize2inds  27163  cusgrfi  27168  fusgrn0degnn0  27209  uspgrloopvtxel  27226  vtxdginducedm1lem4  27252  uhgr0edg0rgrb  27284  wlkl1loop  27347  wlk1walk  27348  upgriswlk  27350  upgrwlkvtxedg  27354  uspgr2wlkeq  27355  wlkv0  27360  wlklenvclwlkOLD  27365  wlksoneq1eq2  27374  wlkon2n0  27376  wlkreslem  27379  wlkres  27380  lfgrwlkprop  27397  pthdivtx  27438  2pthnloop  27440  spthonepeq  27461  uhgrwkspthlem2  27463  uhgrwkspth  27464  usgr2wlkneq  27465  usgr2trlncl  27469  usgr2pthlem  27472  usgr2pth  27473  cyclnspth  27509  lfgrn1cycl  27511  usgr2trlncrct  27512  uspgrn2crct  27514  crctcshwlkn0lem3  27518  crctcshwlkn0lem5  27520  wwlknp  27549  wspthneq1eq2  27566  0enwwlksnge1  27570  wlklnwwlkln1  27574  wlkiswwlks2  27581  wlkiswwlksupgr2  27583  wlklnwwlkln2lem  27588  wwlksnred  27598  wwlksnextbi  27600  wwlksnredwwlkn0  27602  wwlksnextwrd  27603  wwlksnextinj  27605  wwlksnextproplem3  27618  wwlksnextprop  27619  wspthsnwspthsnon  27623  wspthsnonn0vne  27624  2pthon3v  27650  umgr2adedgwlkonALT  27654  umgr2wlk  27656  umgr2wlkon  27657  umgrwwlks2on  27664  elwspths2on  27667  usgr2wspthons3  27671  elwwlks2  27673  rusgrnumwwlk  27682  clwwlkccatlem  27695  clwlkclwwlklem2a4  27703  clwlkclwwlklem2a  27704  clwlkclwwlklem2  27706  clwlkclwwlkf1lem3  27712  erclwwlkeqlen  27725  clwwlknwwlksn  27744  loopclwwlkn1b  27748  clwwlkf1  27756  wwlksext2clwwlk  27764  eleclclwwlknlem2  27768  umgr2cwwk2dif  27771  eleclclwwlkn  27783  hashecclwwlkn1  27784  umgrhashecclwwlk  27785  clwwlknonwwlknonb  27813  clwwlknonex2lem2  27815  clwwlknonex2  27816  1pthon2v  27860  upgr3v3e3cycl  27887  uhgr3cyclexlem  27888  uhgr3cyclex  27889  eupth2lem3lem4  27938  frgr3vlem1  27980  frgr3vlem2  27981  3vfriswmgrlem  27984  3vfriswmgr  27985  3cyclfrgrrn1  27992  n4cyclfrgr  27998  frgrncvvdeqlem3  28008  frgrncvvdeqlem6  28011  frgrncvvdeqlem7  28012  frgrncvvdeqlem8  28013  frgrwopreglem4a  28017  frgrwopreglem3  28021  frgrwopreg1  28025  frgrwopreg2  28026  frgrwopreglem5lem  28027  frgrwopreglem5ALT  28029  frgrwopreg  28030  fusgr2wsp2nb  28041  2wspmdisj  28044  numclwwlk1lem2foa  28061  numclwwlk1lem2f1  28064  numclwwlk1lem2fo  28065  numclwwlk1  28068  wlkl0  28074  numclwwlk2lem1  28083  numclwlk2lem2f  28084  numclwlk2lem2f1o  28086  frgrreg  28101  frgrregord013  28102  frgrregord13  28103  friendshipgt3  28105  friendship  28106  eulplig  28190  ipassi  28546  ubthlem2  28576  isch3  28946  shintcli  29034  shmodsi  29094  spansncvi  29357  hoaddsub  29521  eigorthi  29542  pjss2coi  29869  pjnormssi  29873  pj3cor1i  29914  strb  29963  dmdmd  30005  mdsl0  30015  csmdsymi  30039  chrelat2i  30070  mdsymlem3  30110  mdsymlem6  30113  sumdmdlem2  30124  opreu2reuALT  30168  ssrelf  30295  spthcycl  32274  loop1cycl  32282  cvmlift2lem1  32447  satfrel  32512  satfrnmapom  32515  fmlafvel  32530  fmla1  32532  gonarlem  32539  gonar  32540  goalrlem  32541  goalr  32542  satffunlem  32546  satffunlem1lem1  32547  satffunlem2lem1  32549  satffun  32554  satefvfmla1  32570  mrsubvrs  32667  mclsax  32714  3ccased  32847  dfon2lem3  32928  rdgprc  32937  trpredmintr  32968  trpredrec  32975  frr3g  33019  sltval2  33061  nolt02o  33097  sslttr  33166  scutun12  33169  cgrextend  33367  btwndiff  33386  btwnconn1lem12  33457  brsegle  33467  broutsideof2  33481  funray  33499  elicc3  33563  nn0prpwlem  33568  nn0prpw  33569  fnessref  33603  neibastop2lem  33606  filnetlem4  33627  meran1  33657  waj-ax  33660  arg-ax  33662  bj-con2com  33794  bj-axdd2  33824  bj-alrimg  33850  bj-exlimg  33854  bj-exalimi  33864  bj-cbvalimt  33870  bj-eximcom  33874  bj-ssbid1ALT  33896  bj-sb  33919  bj-dtru  34037  bj-snsetex  34173  bj-restpw  34278  bj-finsumval0  34456  mptsnunlem  34502  icoreclin  34521  relowlpssretop  34528  inunissunidif  34539  rdgssun  34542  finorwe  34546  domalom  34568  wl-dral1d  34653  wl-exeq  34656  wl-lem-exsb  34684  poimirlem29  34803  poimirlem32  34806  fdc  34903  seqpo  34905  incsequz  34906  isismty  34962  ismtybndlem  34967  heibor1lem  34970  ismgmOLD  35011  isexid2  35016  ghomco  35052  pridlc  35232  relcnveq3  35461  elrelscnveq3  35613  cdleme18d  37313  tendovalco  37783  cdlemn11pre  38228  dihord2pre  38243  nnadddir  39043  incssnn0  39188  fphpd  39293  jm2.19lem3  39468  setindtr  39501  islssfg2  39551  mpaaeu  39630  pr2cv  39787  refimssco  39847  iunrelexpmin1  39933  iunrelexpmin2  39937  trclimalb2  39951  clsk1indlem3  40273  syldbl2  40399  tfindsd  40444  mnurndlem1  40497  nzss  40529  sb5ALT  40739  truniALT  40755  ee223  40848  3orbi123VD  41064  sbc3orgVD  41065  exbirVD  41067  exbiriVD  41068  sbcim2gVD  41089  trsbcVD  41091  truniALTVD  41092  onfrALTlem3VD  41101  onfrALTlem2VD  41103  csbrngVD  41110  19.41rgVD  41116  ax6e2eqVD  41121  ax6e2ndeqVD  41123  2uasbanhVD  41125  sb5ALTVD  41127  vk15.4jVD  41128  infxrunb3rnmpt  41582  stoweidlem26  42192  hirstL-ax3  43009  rexsb  43178  rexrsb  43179  euoreqb  43189  2reu8i  43193  afvres  43252  tz6.12-afv  43253  afvco2  43256  afv2orxorb  43308  afv2res  43319  tz6.12-afv2  43320  tz6.12i-afv2  43323  dfatcolem  43335  zm1nn  43383  fzoopth  43408  2ffzoeq  43409  smonoord  43412  iccpartiltu  43429  iccpartlt  43431  iccpartltu  43432  iccpartgtl  43433  iccpartgt  43434  iccpartleu  43435  iccpartgel  43436  icceuelpart  43443  iccpartnel  43445  lswn0  43451  ichnreuop  43481  ichreuopeq  43482  prsprel  43496  sprsymrelfvlem  43499  sprsymrelf1lem  43500  sprsymrelfolem2  43502  prproropf1olem4  43515  paireqne  43520  prprelb  43525  reupr  43531  goldbachth  43556  odz2prm2pw  43572  fmtno4prmfac  43581  fmtno4prmfac193  43582  prmdvdsfmtnof1lem2  43594  2pwp1prmfmtno  43599  lighneallem2  43618  lighneallem4b  43621  lighneallem4  43622  requad2  43635  odd2prm2  43730  mogoldbblem  43732  gbepos  43770  gbowgt5  43774  gbowge7  43775  stgoldbwt  43788  sbgoldbwt  43789  sbgoldbst  43790  sbgoldbaltlem1  43791  sbgoldbalt  43793  sbgoldbo  43799  nnsum3primesle9  43806  nnsum4primesodd  43808  nnsum4primesoddALTV  43809  nnsum4primeseven  43812  nnsum4primesevenALTV  43813  bgoldbtbndlem1  43817  bgoldbtbndlem2  43818  bgoldbtbndlem3  43819  bgoldbtbnd  43821  isomuspgrlem1  43839  upgrwlkupwlk  43862  uspgrsprf1  43869  mgmhmlin  43900  issubmgm2  43904  lmod0rng  44037  lidldomn1  44090  lidlmmgm  44094  rnghmsscmap  44143  rnghmsubcsetclem2  44145  rngcinv  44150  rngccatidALTV  44158  rngcinvALTV  44162  funcrngcsetc  44167  funcrngcsetcALT  44168  rhmsscmap  44189  rhmsubcsetclem2  44191  rhmsubcrngclem2  44197  ringcinv  44201  ringcbasbas  44203  funcringcsetc  44204  funcringcsetcALTV2lem9  44213  ringccatidALTV  44221  ringcinvALTV  44225  ringcbasbasALTV  44227  rhmsubclem4  44258  rhmsubcALTVlem4  44276  ztprmneprm  44293  pgrpgt2nabl  44312  lmodvsmdi  44328  ply1mulgsumlem2  44339  lincsumcl  44384  ellcoellss  44388  linindslinci  44401  islinindfis  44402  lincext3  44409  lindslinindimp2lem4  44414  lindslinindsimp2lem5  44415  lindslinindsimp2  44416  lindsrng01  44421  ldepspr  44426  lincresunit3lem1  44432  elfzolborelfzop1  44472  dignn0ldlem  44560  nn0sumshdiglem1  44579  rrx2xpref1o  44603  rrx2plord2  44607  rrx2plordisom  44608  line2ylem  44636  line2xlem  44638  line2y  44640  itschlc0xyqsol1  44651  inlinecirc02plem  44671  tfis2d  44681  onsetrec  44708
  Copyright terms: Public domain W3C validator