HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem com12 26
Description: Inference that swaps (commutes) antecedents in an implication. (The proof was shortened by Wolf Lammen, 4-Aug-2012.)
Hypothesis
Ref Expression
com12.1
Assertion
Ref Expression
com12

Proof of Theorem com12
StepHypRef Expression
1 id 18 . 2
2 com12.1 . 2
31, 2syl5com 25 1
Colors of variables: wff set class
Syntax hints:   wi 4
This theorem is referenced by:  syl5 27  syl6com 30  mpcom 31  syli 32  pm2.27 34  pm2.43b 45  syl9r 66  com3r 72  pm2.86i 91  pm2.24 99  con3rr3 125  expt 145  jad 151  pm2.61 160  syl5ibcom 209  syl5ibrcom 211  biimprcdOLD 215  pm5.501 331  jaod 371  orel1 372  pm2.62 399  pm2.621OLD 402  impcom 419  imp3a 420  expcom 424  exp3a 425  pm3.21 432  imdistanri 672  pm2.64 734  pm2.75 795  ccased 891  dedlem0b 897  3impd 1137  3expd 1140  mp3an1i 1241  meredith 1257  simplbi2com 1337  a9wa9lem2 1444  a9wa9lem2OLD 1445  a9wa9lem6OLD 1450  hbimd 1544  19.21t 1547  equtrr 1564  sbequ2 1609  ax11b 1652  sb6rf 1694  sb56 1700  exmoeu 1862  moimv 1868  eupickbi 1886  2eu1 1900  exists2 1910  r19.12 2242  2gencl 2363  3gencl 2364  rcla4cv 2418  ceqex 2433  euind 2489  reuind 2500  sseq2 2677  uniiunlem 2729  uneqdifeq 2981  difsn 3163  eqsn 3178  preq12b 3187  intab 3276  iinss2 3329  trint0 3443  dtru 3512  sspwb 3531  copsexg 3556  pocl 3620  pofun 3629  solin 3637  frss 3653  fr2nr 3657  efrirr 3660  tz7.7 3704  ordtri3 3714  ordtr2 3722  suc11 3779  onssneli 3785  eusv2 3829  ralxfrALT 3855  iunpw 3876  fr3nr 3877  ordom 3967  peano5 3981  2optocl 4077  3optocl 4078  ssrel 4091  ssrelrel 4100  relop 4135  sotri3 4334  xp11 4364  relcnvtr 4426  fss 4569  fv3 4687  tz6.12-1 4690  tz6.12c 4694  tz6.12i 4695  fvco2 4735  fvopab2 4752  fornex 4802  funfvima 4857  fvclss 4861  f1fveq 4887  isotr 4912  isotrALT 4913  isomin 4914  oprabid 4945  ovg 5010  poxp 5270  soxp 5271  iotaval 5288  smores 5322  smoel 5330  smogt 5337  smoiso2 5339  smoge 5340  tfrlem2 5342  tfrlem9 5350  tfr3 5357  tz7.48-2 5386  tz7.48-3 5388  tz7.49 5389  abianfp 5392  oecl 5441  oaordex 5461  oalimcl 5463  oaass 5464  oarec 5465  omordi 5466  omlimcl 5478  odi 5479  omeulem1 5482  oen0 5485  oewordri 5491  oeworde 5492  oaabs 5528  omsmolem 5532  2ecoptocl 5599  3ecoptocl 5600  eceqoveq 5614  th3qlem2 5616  dom3d 5720  xpdom2 5764  infensuc 5886  php 5892  onomeneq 5897  unxpdomlem2 5911  unxpdomlem3 5912  isinf 5921  domfi 5930  findcard2 5938  unblem2 5949  unifi 5967  indexfi 5970  supub 6012  suplub 6013  supsnALT 6027  ordiso 6028  ordtypelem3 6031  ordtypelem4 6032  ordtypelem6 6034  ordtypelem7 6035  ordtype 6036  hartogs 6038  card2on 6041  card2inf 6042  elirrv 6048  inf3lem1 6066  inf3lem2 6067  inf3lem3 6068  inf3lem5 6070  noinfep 6094  noinfepOLD 6095  trcl 6096  tcel 6115  r1sdom 6126  rankr1c 6166  rankval3b 6169  rankr1 6177  rankel 6183  rankxpsuc 6223  scottex 6226  carddomi2 6266  ondomcard 6274  pr2ne 6289  dif1card 6291  aceq3lem 6322  aceq8clem 6337  fodomnum 6345  cardaleph 6350  cflim2 6421  cfsmolem 6427  domtriomlem 6440  axdc3lem4 6450  axdc4lem 6452  kmlem4 6484  kmlem9 6489  kmlem12 6492  kmlem13 6493  numthlem 6499  zorn2lem3 6506  zorn2lem4 6507  zorn2lem5 6508  zorn2lem6 6509  zorn2lem7 6510  zornn0 6514  axdclem 6515  axdclem2 6516  ondomon 6551  alephval2 6558  cfpwsdom 6585  axrepnd 6595  tsksdom 6646  tskr1om 6657  grupr 6687  gruiun 6689  ingru 6704  grothomex 6718  indpi 6798  nqereu 6821  genpnnp 6897  prlem934 6925  ltaddpr2 6927  reclem2pr 6940  mulgt0sr 6996  supsrlem 7002  mul0ori 7465  lemul1a 7602  squeeze0 7666  peano5nni 7715  nnunb 7879  fzind 8009  nn0ind-raph 8012  zindd 8013  eluzadd 8072  uzin 8075  iccss2 8344  icoshft 8376  fzen 8428  fzss1 8445  expcllem 8646  expeq0 8661  mulexp 8670  expword2i 8687  bernneq 8749  facdiv 8780  hashmap 8840  cjexp 8925  absexp 9056  abssubne0 9073  sin01gt0 9525  alzdvds 9631  dvdslegcd 9666  gcdneg 9675  rprimelpwr 9704  qredeq 9750  exprmfctlem 9753  prmpwdvds 9862  prmreclem4 9877  pslem 10189  spwmo 10200  gxnn0add 10695  gxnn0mul 10698  ismgm 10747  isexid2 10752  isga 10803  gagrpid 10811  gaass 10812  gapmlem 10814  rngodm1dm2 10867  rngosn4 10878  fiinopn 10908  tgcl 10953  tgss2 10967  distop 10978  ssnei2 11068  opnnei 11072  cnpnei 11125  cnpco 11128  cncnplem2 11134  cncmp 11161  cmpfi 11174  usinuniop 11179  dfcon2 11180  cnmptcom 11225  fbfinnfr 11254  isfildlem 11264  snfil 11272  fbunfip 11275  fgfild 11283  limfilss 11295  elfm2 11310  flimopn 11317  meteq0 11342  neibl 11413  reconn 11488  pi1gplem 11579  caubl 11637  ipassi 11976  ubthlem2 12007  minveclem5 12017  volsuplem 12183  cxpmul2 12812  qabvexp 12964  isch3 13307  shintcli 13395  shmodsi 13455  spansncvi 13736  pjjsi 13784  hoaddsub 13883  eigorthi 13904  homco2 14043  cnlnadjlem5 14137  pjss2coi 14230  pjnormssi 14234  pj3cor1i 14275  strb 14324  dmdmd 14366  mdsl0 14376  csmdsymi 14400  chrelat2i 14431  cvati 14432  mdsymlem3 14471  mdsymlem6 14474  sumdmdlem2 14485  dmdbr5ati 14488  3ccased 14656  dedekind 14662  dfres3 14700  dfon2lem3 14730  omssadd 14743  rdgprc 14752  trpredmintr 14839  trpredrec 14846  wfr3g 14860  wfrlem12 14872  frr3g 14885  frrlem11 14898  sltval2 14914  axfelem13 14963  elfuns 15065  axcontlem4 15203  cgrextend 15239  btwndiff 15258  btwnconn1lem12 15329  brsegle 15339  broutsideof2 15353  funray 15371  meran1 15533  waj-ax 15536  arg-ax 15538  wl-pm2.86i 15581  copsexgb 15621  evpexun 15649  cpref 15703  inttr 15708  isunscov 15710  restidsing 15714  twsymr 15716  prj1b 15717  prj3 15718  set2elt 15730  fixpc 15738  surjsec 15766  injrec2 15767  surjsec2 15768  elovdm2 15776  domintrefc 15777  mapmapmap 15802  injsurinj 15803  repfuntw 15815  repcpwti 15816  cbcpcp 15817  unprj 15822  prl 15823  prl2 15825  prjmapcp2 15826  dstr 15827  nZdef 15836  jidd 15848  midd 15849  preotr2 15883  int2pre 15885  ubpar 15911  inposet 15928  tolat 15939  pospos 15943  toplat 15946  latdir 15951  ridlideq 15993  rzrlzreq 15994  resgcom 16009  symgfo 16027  curgrpact 16032  grpodivone 16033  grpodivfo 16034  rltrran 16075  zerdivemp1 16097  zintdom 16099  muldisc 16141  svli2 16144  svs2 16147  truni1 16165  truni2 16166  truni3 16167  inttop2 16175  npmp 16181  mapdiscnlem 16188  mapdiscn 16189  mapudiscn 16190  nsn 16192  top2ind 16217  top2usne 16218  homindlem3 16220  intopcoaconlem3b 16221  intopcoaconc 16224  qusp 16225  intcont 16226  prtoptop 16232  prcnt 16234  efilcp 16235  fisub 16237  fbaslim2 16244  limfilnei 16251  conttnf 16252  iscnp3 16254  cnpfillim4 16255  cmptdst 16259  limhun 16261  exopcopn 16263  prdnei 16264  limptlimpr2lem1 16265  limptlimpr2lem2 16266  flimfnei2 16268  islimrs 16271  islimrs3 16272  islimrs4 16273  bwt2 16288  grpohmlem1 16313  grpohmlem2 16314  grpohmlem3 16315  grpohmlem4 16316  grpohmlem5 16317  grpohm 16318  iintlem1 16338  iint 16340  cnvtr 16344  mlteqer 16345  xrletr2 16346  lteqtpos 16351  lvsovso 16367  lvsovso3 16369  supnuf 16370  claddrvr 16389  sigadd 16390  addcomv 16396  addcanrg 16408  negveudr 16410  subclrvd 16415  distsava 16430  intvconlem1 16446  consuba 16449  hdrmp 16452  cmppfd 16494  domcmpd 16495  codcmpd 16496  cmpasso 16522  cmpida 16523  cmpidb 16524  dualalg 16533  dualded 16534  dualcat2 16535  cmpassoh 16552  homgrf 16553  imonclem 16564  cmpmon 16566  iepiclem 16574  isepic 16575  idfisf 16591  propsrc 16616  partarelt1 16642  inttaror 16646  inttarcar 16647  fnctartar 16653  fnctartar2 16654  prismorcset2 16665  morexcmp 16714  cmpmor 16722  setiscat 16726  lemindclsbu 16777  indcls2 16778  clscnc 16792  pgapspf2 16835  elicc3 16868  fictb 16873  finsschain 16874  nn0prpwlem 16881  nn0prpw 16882  2ndcctbss 16941  fnetr 16958  topbasfne 16962  fnessref 16966  neibastop1 16981  neibastop2lem2 16983  neibastop2lem3 16984  neibastop3 16987  topmtcl 16988  fnejoin1 16993  fnejoin2 16994  t0dist 17004  t1sep 17009  regsep 17013  nrmsep 17017  nrmsep2 17018  fmfnfmlem1 17059  flimfbas 17066  fclsfnflim 17079  fcluscomplem 17085  fzmul 17225  fdc 17239  seqpo 17241  incsequz 17242  heibor1lem 17302  ghomco 17344  zerdivemp1x 17357  pridlc 17467  ceqsex3OLD 17497  fphpd 17650  jm2.19lem3 17874  setindtr 17907  infpssrlem3 17953  fin23lem6 17966  fin56 18058  fin1a2lem6 18066  fin1a2lem10 18070  fin1a2lem12 18072  pm14.24 18176  sb5ALT 18274  truniALT 18291  onfrALTlem3 18295  ee223 18367  3orbi123VD 18515  sbc3orgVD 18516  exbirVD 18518  exbiriVD 18519  sbcim2gVD 18540  trsbcVD 18542  truniALTVD 18543  onfrALTlem3VD 18552  onfrALTlem2VD 18554  csbrngVD 18561  19.41rgVD 18567  a9e2eqVD 18572  a9e2ndeqVD 18574  2uasbanhVD 18576  sb5ALTVD 18577  vk15.4jVD 18578  cdleme18d 21476  tendovalco 21970  cdlemn11pre 22427  dihord2pre 22442
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
Copyright terms: Public domain