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  1129  3expd  1132  mp3an1i  1233  simplbi2com  1313  meredith  1317  a9wa9lem2  1545  a9wa9lem5  1548  a9wa9lem15  1558  a9wa9  1562  ax10lem3  1571  ax10  1588  a9wa9lem2OLD  1596  hbimd  1685  19.21t  1688  equtrr  1705  sbequ2  1758  ax11b  1805  sb6rf  1847  sb56  1853  exmoeu  2017  moimv  2023  eupickbi  2041  2eu1  2055  exists2  2065  r19.12  2403  2gencl  2528  3gencl  2529  rcla4cv  2583  ceqex  2598  mob  2651  euind  2656  reuind  2667  sseq2  2853  uniiunlem  2908  uneqdifeq  3171  difsn  3373  eqsn  3389  preq12b  3400  intab  3498  iinss2  3555  trint0  3676  dtru  3745  sspwb  3764  copsexg  3792  pocl  3860  pofun  3869  solin  3876  frss  3899  tz7.7  3957  ordtri3  3967  ordtr2  3975  suc11  4033  onssneli  4039  eusv2  4083  ralxfrALT  4109  iunpw  4130  ordom  4225  peano5  4239  2optocl  4340  3optocl  4341  ssrel  4352  ssrelrel  4361  relop  4408  eliniseg2  4594  sotri3  4616  poltletr  4621  xp11  4654  relcnvtr  4726  fss  4874  fv3  5008  tz6.12-1  5011  tz6.12c  5015  tz6.12i  5016  fvopab2  5071  fornex  5137  funfvima  5201  fvclss  5207  f1fveq  5234  isotr  5273  isotrALT  5274  isoselem  5279  oprabid  5317  ovg  5387  mpteqb  5523  poxp  5719  soxp  5720  sorpsscmpl  5737  iotaval  5751  onnseq  5787  smores  5795  smoel  5803  smogt  5810  smoiso2  5812  tfrlem2  5818  tfr3  5841  tz7.48-2  5878  tz7.48-3  5880  tz7.49  5881  abianfp  5895  oecl  5954  oaordex  5974  oalimcl  5976  oaass  5977  omordi  5982  omlimcl  5994  odi  5995  omeulem1  5998  oen0  6002  oewordri  6008  nnawordi  6037  nnaass  6038  nnmordi  6047  omabs  6061  omsmolem  6067  2ecoptocl  6145  3ecoptocl  6146  eceqoveq  6160  th3qlem2  6162  undifixp  6240  xpdom2  6341  xpf1o  6454  infensuc  6470  php  6476  onomeneq  6481  isinf  6504  findcard2  6520  unblem2  6532  unifi  6555  indexfi  6558  finsschain  6580  marypha1  6600  supub  6621  suplub  6622  supsnALT  6637  hartogs  6673  card2on  6682  card2inf  6683  xpwdomg  6713  elirrv  6724  inf3lem1  6742  inf3lem2  6743  inf3lem3  6744  inf3lem5  6746  noinfep  6773  noinfepOLD  6774  trcl  6823  en3lp  6831  tcel  6843  r1sdom  6859  rankonidlem  6912  rankxpsuc  6964  scottex  6967  pr2ne  7045  dif1card  7047  cardaleph  7108  cflim2  7258  cfsmolem  7265  infpssrlem3  7300  isfin7-2  7391  fin1a2lem6  7400  fin1a2lem10  7404  fin1a2lem12  7406  domtriomlem  7436  axdc3lem4  7447  axdc4lem  7449  kmlem4  7483  kmlem9  7488  kmlem12  7491  kmlem13  7492  zorn2lem3  7506  zorn2lem4  7507  zorn2lem5  7508  zorn2lem6  7509  zorn2lem7  7510  zornn0g  7513  axdclem  7527  axdclem2  7528  ondomon  7562  alephval2  7569  cfpwsdom  7582  axrepnd  7592  tskr1om  7716  grupr  7744  gruiun  7746  ingru  7761  grothomex  7775  indpi  7855  nqereu  7877  genpnnp  7953  prlem934  7981  ltaddpr2  7983  reclem2pr  7996  mulgt0sr  8051  supsrlem  8057  mul0ori  8533  lemul1a  8671  squeeze0  8735  peano5nni  8784  nnunb  8971  fzind  9109  nn0ind-raph  9112  zindd  9113  eluzadd  9247  uzin  9251  icoshft  9566  fzen  9617  expcllem  9839  expeq0  9857  mulexp  9866  expword2i  9883  bernneq  9945  facdiv  9978  hashmap  10048  cjexp  10143  absexp  10275  abssubne0  10293  iseraltlem2  10491  sin01gt0  10781  alzdvds  10890  dvdslegcd  10927  gcdneg  10936  rplpwr  10965  qredeq  11015  prmpwdvds  11149  prmreclem4  11164  ramcl  11274  imasleval  11526  drsdirfi  11554  spwmo  11780  mreiincl  13434  fiinopn  13485  tgcl  13530  tgss2  13546  distop  13558  isclo2  13635  ssnei2  13659  opnnei  13663  tgcnp  13729  cnpnei  13740  cncnplem2  13751  cncmp  13797  cmpfi  13815  2ndcctbss  13864  1stcelcls  13906  cnmptcom  14028  fbfinnfr  14104  isfildlem  14117  snfil  14124  fbunfip  14129  fgcl  14138  fbflim2  14191  elfm2  14209  cnpflf2  14222  meteq0  14243  neibl  14314  reconn  14399  caubl  14582  volsuplem  14740  dvnadd  15082  dvnres  15083  cpnord  15087  mpfrcl  15175  ply1divex  15293  cxpmul2  15735  wilthlem3  15912  lgsquad2lem2  16093  qabvexp  16132  gxnn0add  16275  gxnn0mul  16278  ismgm  16321  isexid2  16326  rngodm1dm2  16419  ipassi  16757  ubthlem2  16788  minveclem5  16798  isch3  17160  shintcli  17248  shmodsi  17308  spansncvi  17589  pjjsi  17637  hoaddsub  17736  eigorthi  17757  cnlnadjlem5  17990  pjss2coi  18083  pjnormssi  18087  pj3cor1i  18128  strb  18177  dmdmd  18219  mdsl0  18229  csmdsymi  18253  chrelat2i  18284  cvati  18285  mdsymlem3  18324  mdsymlem6  18327  sumdmdlem2  18338  dmdbr5ati  18341  cvmlift2lem1  18518  3ccased  18756  dedekind  18762  dfres3  18797  dfon2lem3  18825  rdgprc  18836  trpredmintr  18923  trpredrec  18930  wfr3g  18944  wfrlem12  18956  frr3g  18969  frrlem11  18982  sltval2  18998  axfelem13  19047  elfuns  19149  axcontlem4  19288  cgrextend  19324  btwndiff  19343  btwnconn1lem12  19414  brsegle  19424  broutsideof2  19438  funray  19456  meran1  19518  waj-ax  19521  arg-ax  19523  wl-pm2.86i  19566  copsexgb  19601  evpexun  19630  cpref  19682  inttr  19687  isunscov  19689  restidsing  19691  twsymr  19693  prj1b  19694  prj3  19695  set2elt  19707  fixpc  19716  elovdm2  19749  domintrefc  19750  mapmapmap  19775  injsurinj  19776  repfuntw  19788  cbcpcp  19790  prl  19795  prl2  19797  prjmapcp2  19798  dstr  19799  nZdef  19808  jidd  19820  midd  19821  int2pre  19865  ubpar  19891  inposet  19908  tolat  19919  pospos  19923  toplat  19926  latdir  19931  ridlideq  19971  rzrlzreq  19972  resgcom  19987  grpodivone  20009  grpodivfo  20010  rltrran  20051  zerdivemp1  20073  zintdom  20075  muldisc  20121  svli2  20124  svs2  20127  truni1  20145  truni2  20146  truni3  20147  inttop2  20166  npmp  20172  mapudiscn  20179  nsn  20181  top2ind  20205  top2usne  20206  homindlem3  20208  intopcoaconlem3b  20209  intopcoaconc  20212  qusp  20213  intcont  20214  prcnt  20222  efilcp  20223  fisub  20225  iscnp3  20234  cmptdst  20239  exopcopn  20243  prdnei  20244  limptlimpr2lem1  20245  limptlimpr2lem2  20246  islimrs  20251  islimrs3  20252  islimrs4  20253  bwt2  20266  iintlem1  20299  iint  20301  cnvtr  20305  lvsovso  20327  supnuf  20330  claddrvr  20349  sigadd  20350  addcomv  20356  addcanrg  20368  negveudr  20370  subclrvd  20375  distsava  20390  intvconlem1  20406  hdrmp  20409  cmppfd  20448  domcmpd  20449  codcmpd  20450  cmpasso  20476  cmpida  20477  cmpidb  20478  dualalg  20487  dualded  20488  dualcat2  20489  cmpassoh  20506  homgrf  20507  imonclem  20518  cmpmon  20520  iepiclem  20528  isepic  20529  idfisf  20546  issrc  20572  propsrc  20573  partarelt1  20601  inttaror  20605  inttarcar  20606  fnctartar  20612  fnctartar2  20613  prismorcset2  20624  cmpmor  20681  setiscat  20685  lemindclsbu  20736  indcls2  20737  clscnc  20751  pgapspf2  20794  elicc3  20827  nn0prpwlem  20837  nn0prpw  20838  fnetr  20891  topbasfne  20895  fnessref  20899  neibastop1  20914  neibastop2lem2  20916  neibastop2lem3  20917  neibastop3  20920  topmtcl  20921  fnejoin1  20926  fnejoin2  20927  t0dist  20937  t1sep  20942  regsep  20946  nrmsep  20950  nrmsep2  20951  fmfnfmlem1  20966  flimfbas  20973  flimfcls  20989  filnetlem4  21015  fzmul  21130  fdc  21144  seqpo  21146  incsequz  21147  heibor1lem  21207  ghomco  21249  zerdivemp1x  21262  pridlc  21372  ceqsex3OLD  21402  nelss  21439  iscldtop  21485  incssnn0  21529  fphpd  21641  jm2.19lem3  21861  setindtr  21894  dfac21i  21947  aalioulem2  21961  islssfg2  21991  hbtlem5  22154  mpaaeu  22177  pm14.24  22308  hirstL-ax3  22361  sb5ALT  22452  truniALT  22469  onfrALTlem3  22473  ee223  22560  3orbi123VD  22720  sbc3orgVD  22721  exbirVD  22723  exbiriVD  22724  sbcim2gVD  22745  trsbcVD  22747  truniALTVD  22748  onfrALTlem3VD  22757  onfrALTlem2VD  22759  csbrngVD  22766  19.41rgVD  22772  a9e2eqVD  22777  a9e2ndeqVD  22779  2uasbanhVD  22781  sb5ALTVD  22790  vk15.4jVD  22791  cdleme18d  25663  tendovalco  26133  cdlemn11pre  26579  dihord2pre  26594
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
Copyright terms: Public domain