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

Theorem com12 27
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 19 . 2
2 com12.1 . 2
31, 2syl5com 26 1
Colors of variables: wff set class
Syntax hints:   wi 4
This theorem is referenced by:  syl5 28  syl6com 31  mpcom 32  syli 33  pm2.27 35  pm2.43b 46  syl9r 67  com3r 73  pm2.86i 92  pm2.24 100  con3rr3 126  expt 146  jad 152  pm2.61 161  syl5ibcom 209  syl5ibrcom 211  pm5.501 329  jaod 368  orel1 369  pm2.62 396  impcom 415  imp3a 416  expcom 420  exp3a 421  pm3.21 428  imdistanri 668  pm2.64 726  pm2.75 783  ccased 878  dedlem0b 884  3impd 1126  3expd 1129  mp3an1i 1230  meredith 1246  simplbi2com 1326  a9wa9lem2 1433  a9wa9lem2OLD 1434  a9wa9lem6OLD 1439  hbimd 1533  19.21t 1536  equtrr 1553  sbequ2 1598  ax11b 1641  sb6rf 1683  sb56 1689  exmoeu 1851  moimv 1857  eupickbi 1875  2eu1 1889  exists2 1899  r19.12 2231  2gencl 2355  3gencl 2356  rcla4cv 2410  ceqex 2425  mob 2478  euind 2483  reuind 2494  sseq2 2680  uniiunlem 2735  uneqdifeq 2991  difsn 3185  eqsn 3201  preq12b 3212  intab 3310  iinss2 3364  trint0 3480  dtru 3549  sspwb 3568  copsexg 3596  pocl 3659  pofun 3668  solin 3676  frss 3693  fr2nr 3697  efrirr 3700  tz7.7 3744  ordtri3 3754  ordtr2 3762  suc11 3820  onssneli 3826  eusv2 3870  ralxfrALT 3896  iunpw 3917  fr3nr 3918  ordom 4010  peano5 4024  2optocl 4123  3optocl 4124  ssrel 4135  ssrelrel 4144  relop 4191  eliniseg2 4375  sotri3 4395  poltletr 4400  xp11 4434  relcnvtr 4502  fss 4648  fv3 4777  tz6.12-1 4780  tz6.12c 4784  tz6.12i 4785  fvopab2 4839  fornex 4896  funfvima 4957  fvclss 4963  f1fveq 4989  isotr 5020  isotrALT 5021  oprabid 5053  ovg 5122  mpteqb 5256  poxp 5437  soxp 5438  iotaval 5455  smores 5494  smoel 5502  smogt 5509  smoiso2 5511  smoge 5512  tfrlem2 5514  tfrlem9 5522  tfr3 5529  tz7.48-2 5558  tz7.48-3 5560  tz7.49 5561  abianfp 5564  oecl 5614  oaordex 5634  oalimcl 5636  oaass 5637  oarec 5638  omordi 5639  omlimcl 5651  odi 5652  omeulem1 5655  oen0 5658  oewordri 5664  oeworde 5665  oaabs 5701  omsmolem 5705  2ecoptocl 5776  3ecoptocl 5777  eceqoveq 5791  th3qlem2 5793  undifixp 5864  xpdom2 5954  infensuc 6079  php 6085  onomeneq 6090  isinf 6112  findcard2 6128  unblem2 6140  unifi 6162  indexfi 6165  finsschain 6183  supub 6215  suplub 6216  supsnALT 6231  ordiso 6232  ordtypelem3 6235  ordtypelem4 6236  ordtypelem6 6238  ordtypelem7 6239  ordtype 6240  hartogs 6242  card2on 6252  card2inf 6253  elirrv 6259  inf3lem1 6277  inf3lem2 6278  inf3lem3 6279  inf3lem5 6281  noinfep 6307  noinfepOLD 6308  trcl 6309  tcel 6328  r1sdom 6339  rankr1c 6379  rankval3b 6382  rankr1 6390  rankel 6396  rankxpsuc 6436  scottex 6439  ondomcard 6493  pr2ne 6512  dif1card 6514  aceq3lem 6545  aceq8clem 6560  cardaleph 6576  cflim2 6687  cfsmolem 6693  domtriomlem 6706  axdc3lem4 6716  axdc4lem 6718  kmlem4 6750  kmlem9 6755  kmlem12 6758  kmlem13 6759  zorn2lem3 6773  zorn2lem4 6774  zorn2lem5 6775  zorn2lem6 6776  zorn2lem7 6777  zornn0 6781  axdclem 6782  axdclem2 6783  ondomon 6817  alephval2 6824  cfpwsdom 6838  axrepnd 6848  tskr1om 6910  grupr 6938  gruiun 6940  ingru 6955  grothomex 6969  indpi 7049  nqereu 7072  genpnnp 7148  prlem934 7176  ltaddpr2 7178  reclem2pr 7191  mulgt0sr 7247  supsrlem 7253  mul0ori 7725  lemul1a 7863  squeeze0 7927  peano5nni 7976  nnunb 8162  fzind 8298  nn0ind-raph 8301  zindd 8302  eluzadd 8436  uzin 8440  icoshft 8751  fzen 8802  expcllem 9022  expeq0 9038  mulexp 9047  expword2i 9064  bernneq 9126  facdiv 9158  hashmap 9227  cjexp 9320  absexp 9452  abssubne0 9470  iseraltlem2 9669  sin01gt0 9955  alzdvds 10063  dvdslegcd 10100  gcdneg 10109  rprimelpwr 10138  qredeq 10185  exprmfctlem 10188  prmpwdvds 10305  prmreclem4 10320  ramcl 10430  imasleval 10671  drsdirfi 10698  spwmo 10878  gxnn0add 11855  gxnn0mul 11858  ismgm 11901  isexid2 11906  rngodm1dm2 12023  fiinopn 12053  tgcl 12098  tgss2 12114  distop 12126  ssnei2 12222  opnnei 12226  tgcnp 12292  cnpnei 12303  cncnplem2 12314  cncmp 12360  cmpfi 12378  2ndcctbss 12426  1stcelcls 12468  cnmptcom 12590  fbfinnfr 12661  isfildlem 12672  snfil 12680  fbunfip 12683  fgfild 12691  fbflim2 12718  elfm2 12738  cnpflf2 12751  meteq0 12772  neibl 12843  reconn 12928  pi1gplem 13059  caubl 13100  ipassi 13439  ubthlem2 13470  minveclem5 13480  volsuplem 13659  dvnadd 13999  dvnres 14000  cpnord 14004  cxpmul2 14472  qabvexp 14743  isch3 15326  shintcli 15414  shmodsi 15474  spansncvi 15755  pjjsi 15803  hoaddsub 15902  eigorthi 15923  cnlnadjlem5 16156  pjss2coi 16249  pjnormssi 16253  pj3cor1i 16294  strb 16343  dmdmd 16385  mdsl0 16395  csmdsymi 16419  chrelat2i 16450  cvati 16451  mdsymlem3 16490  mdsymlem6 16493  sumdmdlem2 16504  dmdbr5ati 16507  wilthlem3 16650  3ccased 17003  dedekind 17009  dfres3 17045  dfon2lem3 17074  omssadd 17087  rdgprc 17096  trpredmintr 17183  trpredrec 17190  wfr3g 17204  wfrlem12 17216  frr3g 17229  frrlem11 17242  sltval2 17258  axfelem13 17307  elfuns 17409  axcontlem4 17547  cgrextend 17583  btwndiff 17602  btwnconn1lem12 17673  brsegle 17683  broutsideof2 17697  funray 17715  meran1 17877  waj-ax 17880  arg-ax 17882  wl-pm2.86i 17925  copsexgb 17964  evpexun 17993  cpref 18046  inttr 18051  isunscov 18053  restidsing 18055  twsymr 18057  prj1b 18058  prj3 18059  set2elt 18071  fixpc 18080  elovdm2 18113  domintrefc 18114  mapmapmap 18139  injsurinj 18140  repfuntw 18152  cbcpcp 18154  prl 18159  prl2 18161  prjmapcp2 18162  dstr 18163  nZdef 18172  jidd 18184  midd 18185  int2pre 18229  ubpar 18255  inposet 18272  tolat 18283  pospos 18287  toplat 18290  latdir 18295  ridlideq 18335  rzrlzreq 18336  resgcom 18351  grpodivone 18373  grpodivfo 18374  rltrran 18415  zerdivemp1 18437  zintdom 18439  muldisc 18485  svli2 18488  svs2 18491  truni1 18509  truni2 18510  truni3 18511  inttop2 18530  npmp 18536  mapudiscn 18543  nsn 18545  top2ind 18569  top2usne 18570  homindlem3 18572  intopcoaconlem3b 18573  intopcoaconc 18576  qusp 18577  intcont 18578  prcnt 18586  efilcp 18587  fisub 18589  iscnp3 18600  cmptdst 18605  exopcopn 18609  prdnei 18610  limptlimpr2lem1 18611  limptlimpr2lem2 18612  flfnei2 18614  islimrs 18617  islimrs3 18618  islimrs4 18619  bwt2 18632  iintlem1 18665  iint 18667  cnvtr 18671  lvsovso 18693  lvsovso3 18695  supnuf 18696  claddrvr 18715  sigadd 18716  addcomv 18722  addcanrg 18734  negveudr 18736  subclrvd 18741  distsava 18756  intvconlem1 18772  hdrmp 18775  cmppfd 18814  domcmpd 18815  codcmpd 18816  cmpasso 18842  cmpida 18843  cmpidb 18844  dualalg 18853  dualded 18854  dualcat2 18855  cmpassoh 18872  homgrf 18873  imonclem 18884  cmpmon 18886  iepiclem 18894  isepic 18895  idfisf 18912  issrc 18938  propsrc 18939  partarelt1 18967  inttaror 18971  inttarcar 18972  fnctartar 18978  fnctartar2 18979  prismorcset2 18990  cmpmor 19047  setiscat 19051  lemindclsbu 19102  indcls2 19103  clscnc 19117  pgapspf2 19160  elicc3 19193  nn0prpwlem 19203  nn0prpw 19204  fnetr 19257  topbasfne 19261  fnessref 19265  neibastop1 19280  neibastop2lem2 19282  neibastop2lem3 19283  neibastop3 19286  topmtcl 19287  fnejoin1 19292  fnejoin2 19293  t0dist 19303  t1sep 19308  regsep 19312  nrmsep 19316  nrmsep2 19317  fmfnfmlem1 19352  flimfbas 19359  flimfcls 19376  filnetlem4 19403  fzmul 19518  fdc 19532  seqpo 19534  incsequz 19535  heibor1lem 19595  ghomco 19637  zerdivemp1x 19650  pridlc 19754  ceqsex3OLD 19784  nelss 19832  xpwdomg 19969  mreiincl 20044  iscldtop 20092  incssnn0 20135  marypha1 20138  fphpd 20253  jm2.19lem3 20473  setindtr 20506  dfac21i 20578  infpssrlem3 20605  fin23lem6 20618  fin56 20708  fin1a2lem6 20716  fin1a2lem10 20720  fin1a2lem12 20722  aalioulem2 20740  islssfg2 20815  mpfrcl 20959  ply1divex 21177  hbtlem5 21314  mpaaeu 21337  pm14.24 21472  hirstL-ax3 21524  sb5ALT 21575  truniALT 21592  onfrALTlem3 21596  ee223 21677  3orbi123VD 21828  sbc3orgVD 21829  exbirVD 21831  exbiriVD 21832  sbcim2gVD 21853  trsbcVD 21855  truniALTVD 21856  onfrALTlem3VD 21865  onfrALTlem2VD 21867  csbrngVD 21874  19.41rgVD 21880  a9e2eqVD 21885  a9e2ndeqVD 21887  2uasbanhVD 21889  sb5ALTVD 21894  vk15.4jVD 21895  cdleme18d 24763  tendovalco 25233  cdlemn11pre 25679  dihord2pre 25694
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
Copyright terms: Public domain