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 15620  evpexun 15650  cpref 15703  inttr 15708  isunscov 15710  restidsing 15714  twsymr 15716  prj1b 15717  prj3 15718  set2elt 15730  fixpc 15739  surjsec 15767  injrec2 15768  surjsec2 15769  elovdm2 15777  domintrefc 15778  mapmapmap 15804  injsurinj 15805  repfuntw 15817  repcpwti 15818  cbcpcp 15819  unprj 15824  prl 15825  prl2 15827  prjmapcp2 15828  dstr 15829  nZdef 15838  jidd 15850  midd 15851  preotr2 15898  int2pre 15900  ubpar 15926  inposet 15943  tolat 15954  pospos 15958  toplat 15961  latdir 15966  ridlideq 16006  rzrlzreq 16007  resgcom 16022  symgfo 16040  curgrpact 16045  grpodivone 16046  grpodivfo 16047  rltrran 16088  zerdivemp1 16110  zintdom 16112  muldisc 16158  svli2 16161  svs2 16164  truni1 16182  truni2 16183  truni3 16184  inttop2 16203  npmp 16209  mapdiscnlem 16216  mapdiscn 16217  mapudiscn 16218  nsn 16220  top2ind 16245  top2usne 16246  homindlem3 16248  intopcoaconlem3b 16249  intopcoaconc 16252  qusp 16253  intcont 16254  prtoptop 16260  prcnt 16262  efilcp 16263  fisub 16265  fbaslim2 16272  limfilnei 16279  conttnf 16280  iscnp3 16282  cnpfillim4 16283  cmptdst 16287  limhun 16289  exopcopn 16291  prdnei 16292  limptlimpr2lem1 16293  limptlimpr2lem2 16294  flimfnei2 16296  islimrs 16299  islimrs3 16300  islimrs4 16301  bwt2 16316  iintlem1 16351  iint 16353  cnvtr 16357  mlteqer 16358  xrletr2 16359  lteqttos 16364  lvsovso 16380  lvsovso3 16382  supnuf 16383  claddrvr 16402  sigadd 16403  addcomv 16409  addcanrg 16421  negveudr 16423  subclrvd 16428  distsava 16443  intvconlem1 16459  consuba 16462  hdrmp 16465  cmppfd 16507  domcmpd 16508  codcmpd 16509  cmpasso 16535  cmpida 16536  cmpidb 16537  dualalg 16546  dualded 16547  dualcat2 16548  cmpassoh 16565  homgrf 16566  imonclem 16577  cmpmon 16579  iepiclem 16587  isepic 16588  idfisf 16605  issrc 16631  propsrc 16632  partarelt1 16660  inttaror 16664  inttarcar 16665  fnctartar 16671  fnctartar2 16672  prismorcset2 16683  morexcmp 16732  cmpmor 16740  setiscat 16744  lemindclsbu 16795  indcls2 16796  clscnc 16810  pgapspf2 16853  elicc3 16886  fictb 16891  finsschain 16892  nn0prpwlem 16899  nn0prpw 16900  2ndcctbss 16959  fnetr 16976  topbasfne 16980  fnessref 16984  neibastop1 16999  neibastop2lem2 17001  neibastop2lem3 17002  neibastop3 17005  topmtcl 17006  fnejoin1 17011  fnejoin2 17012  t0dist 17022  t1sep 17027  regsep 17031  nrmsep 17035  nrmsep2 17036  fmfnfmlem1 17077  flimfbas 17084  fclsfnflim 17097  fcluscomplem 17103  fzmul 17243  fdc 17257  seqpo 17259  incsequz 17260  heibor1lem 17320  ghomco 17362  zerdivemp1x 17375  pridlc 17485  ceqsex3OLD 17515  fphpd 17668  jm2.19lem3 17892  setindtr 17925  infpssrlem3 17971  fin23lem6 17984  fin56 18076  fin1a2lem6 18084  fin1a2lem10 18088  fin1a2lem12 18090  aalioulem2 18118  mpaaeu 18192  pm14.24 18376  sb5ALT 18474  truniALT 18491  onfrALTlem3 18495  ee223 18568  3orbi123VD 18716  sbc3orgVD 18717  exbirVD 18719  exbiriVD 18720  sbcim2gVD 18741  trsbcVD 18743  truniALTVD 18744  onfrALTlem3VD 18753  onfrALTlem2VD 18755  csbrngVD 18762  19.41rgVD 18768  a9e2eqVD 18773  a9e2ndeqVD 18775  2uasbanhVD 18777  sb5ALTVD 18779  vk15.4jVD 18780  cdleme18d 21678  tendovalco 22172  cdlemn11pre 22629  dihord2pre 22644
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
Copyright terms: Public domain