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 208  syl5ibrcom 210  pm5.501 328  jaod 367  orel1 368  pm2.62 395  impcom 414  imp3a 415  expcom 419  exp3a 420  pm3.21 427  imdistanri 667  pm2.64 725  pm2.75 782  ccased 877  dedlem0b 883  3impd 1125  3expd 1128  mp3an1i 1229  meredith 1245  simplbi2com 1325  a9wa9lem2 1432  a9wa9lem2OLD 1433  a9wa9lem6OLD 1438  hbimd 1532  19.21t 1535  equtrr 1552  sbequ2 1597  ax11b 1640  sb6rf 1682  sb56 1688  exmoeu 1850  moimv 1856  eupickbi 1874  2eu1 1888  exists2 1898  r19.12 2229  2gencl 2350  3gencl 2351  rcla4cv 2405  ceqex 2420  mob 2473  euind 2478  reuind 2489  sseq2 2675  uniiunlem 2727  uneqdifeq 2980  difsn 3162  eqsn 3178  preq12b 3187  intab 3276  iinss2 3329  trint0 3443  dtru 3512  sspwb 3531  copsexg 3556  pocl 3620  pofun 3629  solin 3637  frss 3654  fr2nr 3658  efrirr 3661  tz7.7 3705  ordtri3 3715  ordtr2 3723  suc11 3781  onssneli 3787  eusv2 3831  ralxfrALT 3857  iunpw 3878  fr3nr 3879  ordom 3971  peano5 3985  2optocl 4082  3optocl 4083  ssrel 4096  ssrelrel 4105  relop 4147  eliniseg2 4328  sotri3 4347  xp11 4378  relcnvtr 4441  fss 4585  fv3 4705  tz6.12-1 4708  tz6.12c 4712  tz6.12i 4713  fvopab2 4771  fornex 4821  funfvima 4876  fvclss 4880  f1fveq 4906  isotr 4932  isotrALT 4933  isomin 4934  oprabid 4965  ovg 5032  mpteqb 5161  poxp 5329  soxp 5330  iotaval 5347  smores 5383  smoel 5391  smogt 5398  smoiso2 5400  smoge 5401  tfrlem2 5403  tfrlem9 5411  tfr3 5418  tz7.48-2 5447  tz7.48-3 5449  tz7.49 5450  abianfp 5453  oecl 5502  oaordex 5522  oalimcl 5524  oaass 5525  oarec 5526  omordi 5527  omlimcl 5539  odi 5540  omeulem1 5543  oen0 5546  oewordri 5552  oeworde 5553  oaabs 5589  omsmolem 5593  2ecoptocl 5664  3ecoptocl 5665  eceqoveq 5679  th3qlem2 5681  dom3d 5788  xpdom2 5835  infensuc 5957  php 5963  onomeneq 5968  unxpdomlem2 5982  unxpdomlem3 5983  isinf 5992  domfi 6001  findcard2 6009  unblem2 6021  unifi 6039  indexfi 6042  supub 6088  suplub 6089  supsnALT 6103  ordiso 6104  ordtypelem3 6107  ordtypelem4 6108  ordtypelem6 6110  ordtypelem7 6111  ordtype 6112  hartogs 6114  card2on 6117  card2inf 6118  elirrv 6124  inf3lem1 6142  inf3lem2 6143  inf3lem3 6144  inf3lem5 6146  noinfep 6170  noinfepOLD 6171  trcl 6172  tcel 6191  r1sdom 6202  rankr1c 6242  rankval3b 6245  rankr1 6253  rankel 6259  rankxpsuc 6299  scottex 6302  carddomi2 6342  ondomcard 6350  pr2ne 6366  dif1card 6368  aceq3lem 6399  aceq8clem 6414  fodomnum 6422  cardaleph 6427  cflim2 6524  cfsmolem 6530  domtriomlem 6543  axdc3lem4 6553  axdc4lem 6555  kmlem4 6587  kmlem9 6592  kmlem12 6595  kmlem13 6596  zorn2lem3 6608  zorn2lem4 6609  zorn2lem5 6610  zorn2lem6 6611  zorn2lem7 6612  zornn0 6616  axdclem 6617  axdclem2 6618  ondomon 6653  alephval2 6660  cfpwsdom 6687  axrepnd 6697  tsksdom 6748  tskr1om 6759  grupr 6788  gruiun 6790  ingru 6805  grothomex 6819  indpi 6899  nqereu 6922  genpnnp 6998  prlem934 7026  ltaddpr2 7028  reclem2pr 7041  mulgt0sr 7097  supsrlem 7103  mul0ori 7566  lemul1a 7703  squeeze0 7767  peano5nni 7816  nnunb 7980  fzind 8111  nn0ind-raph 8114  zindd 8115  eluzadd 8174  uzin 8177  iccss2 8446  icoshft 8478  fzen 8530  fzss1 8548  expcllem 8750  expeq0 8765  mulexp 8774  expword2i 8791  bernneq 8852  facdiv 8883  hashmap 8949  cjexp 9038  absexp 9169  abssubne0 9186  sin01gt0 9642  alzdvds 9749  dvdslegcd 9785  gcdneg 9794  rprimelpwr 9823  qredeq 9869  exprmfctlem 9872  prmpwdvds 9988  prmreclem4 10003  pslem 10443  spwmo 10454  gxnn0add 11316  gxnn0mul 11319  ismgm 11362  isexid2 11367  rngodm1dm2 11484  rngosn4 11495  fiinopn 11516  tgcl 11561  tgss2 11575  distop 11586  ssnei2 11676  opnnei 11680  cnpnei 11733  cncnplem2 11742  cncmp 11769  cmpfi 11782  usinuniop 11787  dfcon2 11788  cnmptcom 11833  fbfinnfr 11862  isfildlem 11872  snfil 11880  fbunfip 11883  fgfild 11891  limfilss 11903  elfm2 11918  flimopn 11925  meteq0 11949  neibl 12020  reconn 12095  pi1gplem 12186  caubl 12244  ipassi 12583  ubthlem2 12614  minveclem5 12624  volsuplem 12790  cxpmul2 13419  qabvexp 13568  isch3 13917  shintcli 14005  shmodsi 14065  spansncvi 14346  pjjsi 14394  hoaddsub 14493  eigorthi 14514  cnlnadjlem5 14747  pjss2coi 14840  pjnormssi 14844  pj3cor1i 14885  strb 14934  dmdmd 14976  mdsl0 14986  csmdsymi 15010  chrelat2i 15041  cvati 15042  mdsymlem3 15081  mdsymlem6 15084  sumdmdlem2 15095  dmdbr5ati 15098  wilthlem3 15240  3ccased 15574  dedekind 15580  dfres3 15618  dfon2lem3 15648  omssadd 15661  rdgprc 15670  trpredmintr 15757  trpredrec 15764  wfr3g 15778  wfrlem12 15790  frr3g 15803  frrlem11 15816  sltval2 15832  axfelem13 15881  elfuns 15983  axcontlem4 16121  cgrextend 16157  btwndiff 16176  btwnconn1lem12 16247  brsegle 16257  broutsideof2 16271  funray 16289  meran1 16451  waj-ax 16454  arg-ax 16456  wl-pm2.86i 16499  copsexgb 16538  evpexun 16568  cpref 16621  inttr 16626  isunscov 16628  restidsing 16632  twsymr 16634  prj1b 16635  prj3 16636  set2elt 16648  fixpc 16657  elovdm2 16695  domintrefc 16696  mapmapmap 16722  injsurinj 16723  repfuntw 16735  repcpwti 16736  cbcpcp 16737  unprj 16742  prl 16743  prl2 16745  prjmapcp2 16746  dstr 16747  nZdef 16756  jidd 16768  midd 16769  preotr2 16816  int2pre 16818  ubpar 16844  inposet 16861  tolat 16872  pospos 16876  toplat 16879  latdir 16884  ridlideq 16924  rzrlzreq 16925  resgcom 16940  grpodivone 16962  grpodivfo 16963  rltrran 17004  zerdivemp1 17026  zintdom 17028  muldisc 17074  svli2 17077  svs2 17080  truni1 17098  truni2 17099  truni3 17100  inttop2 17119  npmp 17125  mapdiscnlem 17132  mapdiscn 17133  mapudiscn 17134  nsn 17136  top2ind 17161  top2usne 17162  homindlem3 17164  intopcoaconlem3b 17165  intopcoaconc 17168  qusp 17169  intcont 17170  prcnt 17178  efilcp 17179  fisub 17181  fbaslim2 17188  limfilnei 17195  conttnf 17196  iscnp3 17198  cnpfillim4 17199  cmptdst 17203  limhun 17205  exopcopn 17207  prdnei 17208  limptlimpr2lem1 17209  limptlimpr2lem2 17210  flimfnei2 17212  islimrs 17215  islimrs3 17216  islimrs4 17217  bwt2 17232  iintlem1 17267  iint 17269  cnvtr 17273  mlteqer 17274  xrletr2 17275  lteqttos 17280  lvsovso 17296  lvsovso3 17298  supnuf 17299  claddrvr 17318  sigadd 17319  addcomv 17325  addcanrg 17337  negveudr 17339  subclrvd 17344  distsava 17359  intvconlem1 17375  consuba 17378  hdrmp 17381  cmppfd 17423  domcmpd 17424  codcmpd 17425  cmpasso 17451  cmpida 17452  cmpidb 17453  dualalg 17462  dualded 17463  dualcat2 17464  cmpassoh 17481  homgrf 17482  imonclem 17493  cmpmon 17495  iepiclem 17503  isepic 17504  idfisf 17521  issrc 17547  propsrc 17548  partarelt1 17576  inttaror 17580  inttarcar 17581  fnctartar 17587  fnctartar2 17588  prismorcset2 17599  cmpmor 17656  setiscat 17660  lemindclsbu 17711  indcls2 17712  clscnc 17726  pgapspf2 17769  elicc3 17802  fictb 17807  finsschain 17808  nn0prpwlem 17815  nn0prpw 17816  2ndcctbss 17875  fnetr 17892  topbasfne 17896  fnessref 17900  neibastop1 17915  neibastop2lem2 17917  neibastop2lem3 17918  neibastop3 17921  topmtcl 17922  fnejoin1 17927  fnejoin2 17928  t0dist 17938  t1sep 17943  regsep 17947  nrmsep 17951  nrmsep2 17952  fmfnfmlem1 17993  flimfbas 18000  fclsfnflim 18013  fcluscomplem 18019  fzmul 18159  fdc 18173  seqpo 18175  incsequz 18176  heibor1lem 18236  ghomco 18278  zerdivemp1x 18291  pridlc 18401  ceqsex3OLD 18431  fphpd 18581  jm2.19lem3 18802  setindtr 18835  poltletr 18871  infpssrlem3 18948  fin23lem6 18961  fin56 19054  fin1a2lem6 19062  fin1a2lem10 19066  fin1a2lem12 19068  aalioulem2 19096  islssfg2 19171  mpaaeu 19311  pm14.24 19453  sb5ALT 19551  truniALT 19568  onfrALTlem3 19572  ee223 19645  3orbi123VD 19793  sbc3orgVD 19794  exbirVD 19796  exbiriVD 19797  sbcim2gVD 19818  trsbcVD 19820  truniALTVD 19821  onfrALTlem3VD 19830  onfrALTlem2VD 19832  csbrngVD 19839  19.41rgVD 19845  a9e2eqVD 19850  a9e2ndeqVD 19852  2uasbanhVD 19854  sb5ALTVD 19856  vk15.4jVD 19857  cdleme18d 22701  tendovalco 23171  cdlemn11pre 23616  dihord2pre 23631
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
Copyright terms: Public domain