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  simplbi2com 1310  meredith 1314  a9wa9lem2 1545  a9wa9lem2OLD 1546  a9wa9lem6OLD 1551  hbimd 1645  19.21t 1648  equtrr 1665  sbequ2 1710  ax11b 1753  sb6rf 1795  sb56 1801  exmoeu 1963  moimv 1969  eupickbi 1987  2eu1 2001  exists2 2011  r19.12 2343  2gencl 2468  3gencl 2469  rcla4cv 2523  ceqex 2538  mob 2591  euind 2596  reuind 2607  sseq2 2793  uniiunlem 2848  uneqdifeq 3111  difsn 3313  eqsn 3329  preq12b 3340  intab 3438  iinss2 3495  trint0 3615  dtru 3684  sspwb 3703  copsexg 3731  pocl 3796  pofun 3805  solin 3813  frss 3830  fr2nr 3834  efrirr 3837  tz7.7 3881  ordtri3 3891  ordtr2 3899  suc11 3957  onssneli 3963  eusv2 4007  ralxfrALT 4033  iunpw 4054  fr3nr 4055  ordom 4148  peano5 4162  2optocl 4261  3optocl 4262  ssrel 4273  ssrelrel 4282  relop 4329  eliniseg2 4515  sotri3 4535  poltletr 4540  xp11 4573  relcnvtr 4645  fss 4793  fv3 4926  tz6.12-1 4929  tz6.12c 4933  tz6.12i 4934  fvopab2 4989  fornex 5055  funfvima 5118  fvclss 5124  f1fveq 5151  isotr 5190  isotrALT 5191  oprabid 5227  ovg 5297  mpteqb 5433  poxp 5627  soxp 5628  sorpsscmpl 5644  iotaval 5658  onnseq 5694  smores 5702  smoel 5710  smogt 5717  smoiso2 5719  smoge 5720  tfrlem2 5726  tfrlem9 5735  tfr3 5742  tz7.48-2 5773  tz7.48-3 5775  tz7.49 5776  abianfp 5790  oecl 5845  oaordex 5865  oalimcl 5867  oaass 5868  omordi 5873  omlimcl 5885  odi 5886  omeulem1 5889  oen0 5893  oewordri 5899  omabs 5945  omsmolem 5947  2ecoptocl 6018  3ecoptocl 6019  eceqoveq 6033  th3qlem2 6035  undifixp 6112  xpdom2 6209  xpf1o 6320  infensuc 6340  php 6346  onomeneq 6351  isinf 6374  findcard2 6390  unblem2 6402  unifi 6425  indexfi 6428  finsschain 6448  marypha1 6467  supub 6488  suplub 6489  supsnALT 6504  ordiso 6511  ordtypelem3 6514  ordtypelem4 6515  ordtypelem6 6517  ordtypelem7 6518  ordtype 6519  hartogs 6527  card2on 6536  card2inf 6537  xpwdomg 6567  elirrv 6577  inf3lem1 6595  inf3lem2 6596  inf3lem3 6597  inf3lem5 6599  noinfep 6625  noinfepOLD 6626  trcl 6675  tcel 6695  r1sdom 6708  rankr1c 6748  rankval3b 6751  rankr1 6759  rankel 6765  rankxpsuc 6805  scottex 6808  pr2ne 6886  dif1card 6888  dfac8clem 6909  cardaleph 6949  aceq3lem 6978  cflim2 7099  cfsmolem 7106  infpssrlem3 7141  isfin7-2 7232  fin1a2lem6 7241  fin1a2lem10 7245  fin1a2lem12 7247  domtriomlem 7281  axdc3lem4 7292  axdc4lem 7294  kmlem4 7328  kmlem9 7333  kmlem12 7336  kmlem13 7337  zorn2lem3 7351  zorn2lem4 7352  zorn2lem5 7353  zorn2lem6 7354  zorn2lem7 7355  zornn0g 7358  axdclem 7372  axdclem2 7373  ondomon 7407  alephval2 7414  cfpwsdom 7427  axrepnd 7437  tskr1om 7561  grupr 7589  gruiun 7591  ingru 7606  grothomex 7620  indpi 7700  nqereu 7723  genpnnp 7799  prlem934 7827  ltaddpr2 7829  reclem2pr 7842  mulgt0sr 7898  supsrlem 7904  mul0ori 8376  lemul1a 8514  squeeze0 8578  peano5nni 8627  nnunb 8813  fzind 8949  nn0ind-raph 8952  zindd 8953  eluzadd 9087  uzin 9091  icoshft 9403  fzen 9454  expcllem 9676  expeq0 9694  mulexp 9703  expword2i 9720  bernneq 9782  facdiv 9815  hashmap 9885  cjexp 9980  absexp 10112  abssubne0 10130  iseraltlem2 10327  sin01gt0 10616  alzdvds 10724  dvdslegcd 10761  gcdneg 10770  rprimelpwr 10799  qredeq 10847  prmpwdvds 10969  prmreclem4 10984  ramcl 11094  imasleval 11340  drsdirfi 11367  spwmo 11593  mreiincl 13187  fiinopn 13238  tgcl 13283  tgss2 13299  distop 13311  ssnei2 13410  opnnei 13414  tgcnp 13480  cnpnei 13491  cncnplem2 13502  cncmp 13548  cmpfi 13566  2ndcctbss 13614  1stcelcls 13656  cnmptcom 13778  fbfinnfr 13850  isfildlem 13861  snfil 13869  fbunfip 13872  fgfild 13881  fbflim2 13935  elfm2 13955  cnpflf2 13968  meteq0 13989  neibl 14060  reconn 14145  pi1gplem 14276  caubl 14317  volsuplem 14475  dvnadd 14817  dvnres 14818  cpnord 14822  mpfrcl 14910  ply1divex 15021  cxpmul2 15462  wilthlem3 15629  lgsquad2lem2 15787  qabvexp 15826  gxnn0add 15987  gxnn0mul 15990  ismgm 16033  isexid2 16038  rngodm1dm2 16131  ipassi 16469  ubthlem2 16500  minveclem5 16510  isch3 16872  shintcli 16960  shmodsi 17020  spansncvi 17301  pjjsi 17349  hoaddsub 17448  eigorthi 17469  cnlnadjlem5 17702  pjss2coi 17795  pjnormssi 17799  pj3cor1i 17840  strb 17889  dmdmd 17931  mdsl0 17941  csmdsymi 17965  chrelat2i 17996  cvati 17997  mdsymlem3 18036  mdsymlem6 18039  sumdmdlem2 18050  dmdbr5ati 18053  cvmlift2lem1 18225  3ccased 18450  dedekind 18456  dfres3 18492  dfon2lem3 18520  omssadd 18532  rdgprc 18541  trpredmintr 18628  trpredrec 18635  wfr3g 18649  wfrlem12 18661  frr3g 18674  frrlem11 18687  sltval2 18703  axfelem13 18752  elfuns 18854  axcontlem4 18993  cgrextend 19029  btwndiff 19048  btwnconn1lem12 19119  brsegle 19129  broutsideof2 19143  funray 19161  meran1 19223  waj-ax 19226  arg-ax 19228  wl-pm2.86i 19271  copsexgb 19306  evpexun 19335  cpref 19388  inttr 19393  isunscov 19395  restidsing 19397  twsymr 19399  prj1b 19400  prj3 19401  set2elt 19413  fixpc 19422  elovdm2 19455  domintrefc 19456  mapmapmap 19481  injsurinj 19482  repfuntw 19494  cbcpcp 19496  prl 19501  prl2 19503  prjmapcp2 19504  dstr 19505  nZdef 19514  jidd 19526  midd 19527  int2pre 19571  ubpar 19597  inposet 19614  tolat 19625  pospos 19629  toplat 19632  latdir 19637  ridlideq 19677  rzrlzreq 19678  resgcom 19693  grpodivone 19715  grpodivfo 19716  rltrran 19757  zerdivemp1 19779  zintdom 19781  muldisc 19827  svli2 19830  svs2 19833  truni1 19851  truni2 19852  truni3 19853  inttop2 19872  npmp 19878  mapudiscn 19885  nsn 19887  top2ind 19911  top2usne 19912  homindlem3 19914  intopcoaconlem3b 19915  intopcoaconc 19918  qusp 19919  intcont 19920  prcnt 19928  efilcp 19929  fisub 19931  iscnp3 19940  cmptdst 19945  exopcopn 19949  prdnei 19950  limptlimpr2lem1 19951  limptlimpr2lem2 19952  flfnei2 19954  islimrs 19957  islimrs3 19958  islimrs4 19959  bwt2 19972  iintlem1 20005  iint 20007  cnvtr 20011  lvsovso 20033  lvsovso3 20035  supnuf 20036  claddrvr 20055  sigadd 20056  addcomv 20062  addcanrg 20074  negveudr 20076  subclrvd 20081  distsava 20096  intvconlem1 20112  hdrmp 20115  cmppfd 20154  domcmpd 20155  codcmpd 20156  cmpasso 20182  cmpida 20183  cmpidb 20184  dualalg 20193  dualded 20194  dualcat2 20195  cmpassoh 20212  homgrf 20213  imonclem 20224  cmpmon 20226  iepiclem 20234  isepic 20235  idfisf 20252  issrc 20278  propsrc 20279  partarelt1 20307  inttaror 20311  inttarcar 20312  fnctartar 20318  fnctartar2 20319  prismorcset2 20330  cmpmor 20387  setiscat 20391  lemindclsbu 20442  indcls2 20443  clscnc 20457  pgapspf2 20500  elicc3 20533  nn0prpwlem 20543  nn0prpw 20544  fnetr 20597  topbasfne 20601  fnessref 20605  neibastop1 20620  neibastop2lem2 20622  neibastop2lem3 20623  neibastop3 20626  topmtcl 20627  fnejoin1 20632  fnejoin2 20633  t0dist 20643  t1sep 20648  regsep 20652  nrmsep 20656  nrmsep2 20657  fmfnfmlem1 20672  flimfbas 20679  flimfcls 20696  filnetlem4 20723  fzmul 20838  fdc 20852  seqpo 20854  incsequz 20855  heibor1lem 20915  ghomco 20957  zerdivemp1x 20970  pridlc 21080  ceqsex3OLD 21110  nelss 21147  iscldtop 21193  incssnn0 21237  fphpd 21349  jm2.19lem3 21569  setindtr 21602  dfac21i 21661  aalioulem2 21675  islssfg2 21705  hbtlem5 21852  mpaaeu 21875  pm14.24 22010  hirstL-ax3 22062  sb5ALT 22152  truniALT 22169  onfrALTlem3 22173  ee223 22260  3orbi123VD 22420  sbc3orgVD 22421  exbirVD 22423  exbiriVD 22424  sbcim2gVD 22445  trsbcVD 22447  truniALTVD 22448  onfrALTlem3VD 22457  onfrALTlem2VD 22459  csbrngVD 22466  19.41rgVD 22472  a9e2eqVD 22477  a9e2ndeqVD 22479  2uasbanhVD 22481  sb5ALTVD 22490  vk15.4jVD 22491  cdleme18d 25363  tendovalco 25833  cdlemn11pre 26279  dihord2pre 26294
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
Copyright terms: Public domain