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 2352  3gencl 2353  rcla4cv 2407  ceqex 2422  mob 2475  euind 2480  reuind 2491  sseq2 2677  uniiunlem 2730  uneqdifeq 2985  difsn 3171  eqsn 3187  preq12b 3196  intab 3287  iinss2 3341  trint0 3455  dtru 3524  sspwb 3543  copsexg 3568  pocl 3632  pofun 3641  solin 3649  frss 3666  fr2nr 3670  efrirr 3673  tz7.7 3717  ordtri3 3727  ordtr2 3735  suc11 3793  onssneli 3799  eusv2 3843  ralxfrALT 3869  iunpw 3890  fr3nr 3891  ordom 3983  peano5 3997  2optocl 4094  3optocl 4095  ssrel 4108  ssrelrel 4117  opeliunxp2 4152  relop 4162  eliniseg2 4344  sotri3 4363  poltletr 4368  xp11 4400  relcnvtr 4463  fss 4607  fv3 4733  tz6.12-1 4736  tz6.12c 4740  tz6.12i 4741  fvopab2 4799  fornex 4855  funfvima 4910  fvclss 4915  f1fveq 4941  isotr 4967  isotrALT 4968  isomin 4969  oprabid 5000  ovg 5068  mpteqb 5198  poxp 5370  soxp 5371  iotaval 5388  smores 5427  smoel 5435  smogt 5442  smoiso2 5444  smoge 5445  tfrlem2 5447  tfrlem9 5455  tfr3 5462  tz7.48-2 5491  tz7.48-3 5493  tz7.49 5494  abianfp 5497  oecl 5547  oaordex 5567  oalimcl 5569  oaass 5570  oarec 5571  omordi 5572  omlimcl 5584  odi 5585  omeulem1 5588  oen0 5591  oewordri 5597  oeworde 5598  oaabs 5634  omsmolem 5638  2ecoptocl 5709  3ecoptocl 5710  eceqoveq 5724  th3qlem2 5726  undifixp 5795  dom3d 5838  xpdom2 5885  infensuc 6012  php 6018  onomeneq 6023  unxpdomlem2 6037  unxpdomlem3 6038  isinf 6047  domfi 6056  findcard2 6064  unblem2 6076  unifi 6094  indexfi 6097  finsschain 6115  supub 6144  suplub 6145  supsnALT 6159  ordiso 6160  ordtypelem3 6163  ordtypelem4 6164  ordtypelem6 6166  ordtypelem7 6167  ordtype 6168  hartogs 6170  card2on 6180  card2inf 6181  elirrv 6187  inf3lem1 6205  inf3lem2 6206  inf3lem3 6207  inf3lem5 6209  noinfep 6233  noinfepOLD 6234  trcl 6235  tcel 6254  r1sdom 6265  rankr1c 6305  rankval3b 6308  rankr1 6316  rankel 6322  rankxpsuc 6362  scottex 6365  carddomi2 6405  ondomcard 6413  pr2ne 6429  dif1card 6431  aceq3lem 6462  aceq8clem 6477  fodomnum 6485  cardaleph 6490  cflim2 6587  cfsmolem 6593  domtriomlem 6606  axdc3lem4 6616  axdc4lem 6618  kmlem4 6650  kmlem9 6655  kmlem12 6658  kmlem13 6659  zorn2lem3 6671  zorn2lem4 6672  zorn2lem5 6673  zorn2lem6 6674  zorn2lem7 6675  zornn0 6679  axdclem 6680  axdclem2 6681  ondomon 6716  alephval2 6723  cfpwsdom 6750  axrepnd 6760  tsksdom 6811  tskr1om 6822  grupr 6851  gruiun 6853  ingru 6868  grothomex 6882  indpi 6962  nqereu 6985  genpnnp 7061  prlem934 7089  ltaddpr2 7091  reclem2pr 7104  mulgt0sr 7160  supsrlem 7166  mul0ori 7629  lemul1a 7766  squeeze0 7830  peano5nni 7879  nnunb 8045  fzind 8176  nn0ind-raph 8179  zindd 8180  eluzadd 8239  uzin 8242  iccss2 8511  icoshft 8543  fzen 8595  fzss1 8613  expcllem 8816  expeq0 8831  mulexp 8840  expword2i 8857  bernneq 8918  facdiv 8949  hashmap 9015  cjexp 9104  absexp 9235  abssubne0 9252  sin01gt0 9708  alzdvds 9815  dvdslegcd 9851  gcdneg 9860  rprimelpwr 9889  qredeq 9936  exprmfctlem 9939  prmpwdvds 10055  prmreclem4 10070  drsdirfi 10360  pslem 10529  spwmo 10540  ghmnsgima 10769  gxnn0add 11416  gxnn0mul 11419  ismgm 11462  isexid2 11467  rngodm1dm2 11584  rngosn4 11595  fiinopn 11616  tgcl 11661  tgss2 11675  distop 11686  ssnei2 11776  opnnei 11780  tgcnp 11831  cnpnei 11836  cncnplem2 11845  cncmp 11873  cmpfi 11886  usinuniop 11896  dfcon2 11897  consuba 11901  cnmptcom 11969  fbfinnfr 12003  isfildlem 12013  snfil 12021  fbunfip 12024  fgfild 12032  limfilss 12044  elfm2 12059  flimopn 12066  meteq0 12090  neibl 12161  reconn 12236  pi1gplem 12345  caubl 12409  ipassi 12748  ubthlem2 12779  minveclem5 12789  volsuplem 12955  dvnadd 13263  dvnres 13264  cpnord 13268  cxpmul2 13609  qabvexp 13758  isch3 14117  shintcli 14205  shmodsi 14265  spansncvi 14546  pjjsi 14594  hoaddsub 14693  eigorthi 14714  cnlnadjlem5 14947  pjss2coi 15040  pjnormssi 15044  pj3cor1i 15085  strb 15134  dmdmd 15176  mdsl0 15186  csmdsymi 15210  chrelat2i 15241  cvati 15242  mdsymlem3 15281  mdsymlem6 15284  sumdmdlem2 15295  dmdbr5ati 15298  wilthlem3 15440  3ccased 15926  dedekind 15932  dfres3 15970  dfon2lem3 15999  omssadd 16012  rdgprc 16021  trpredmintr 16108  trpredrec 16115  wfr3g 16129  wfrlem12 16141  frr3g 16154  frrlem11 16167  sltval2 16183  axfelem13 16232  elfuns 16334  axcontlem4 16472  cgrextend 16508  btwndiff 16527  btwnconn1lem12 16598  brsegle 16608  broutsideof2 16622  funray 16640  meran1 16802  waj-ax 16805  arg-ax 16807  wl-pm2.86i 16850  copsexgb 16889  evpexun 16918  cpref 16971  inttr 16976  isunscov 16978  restidsing 16982  twsymr 16984  prj1b 16985  prj3 16986  set2elt 16998  fixpc 17007  elovdm2 17043  domintrefc 17044  mapmapmap 17069  injsurinj 17070  repfuntw 17082  repcpwti 17083  cbcpcp 17084  prl 17089  prl2 17091  prjmapcp2 17092  dstr 17093  nZdef 17102  jidd 17114  midd 17115  preotr2 17157  int2pre 17159  ubpar 17185  inposet 17202  tolat 17213  pospos 17217  toplat 17220  latdir 17225  ridlideq 17265  rzrlzreq 17266  resgcom 17281  grpodivone 17303  grpodivfo 17304  rltrran 17345  zerdivemp1 17367  zintdom 17369  muldisc 17415  svli2 17418  svs2 17421  truni1 17439  truni2 17440  truni3 17441  inttop2 17460  npmp 17466  mapdiscnlem 17473  mapdiscn 17474  mapudiscn 17475  nsn 17477  top2ind 17502  top2usne 17503  homindlem3 17505  intopcoaconlem3b 17506  intopcoaconc 17509  qusp 17510  intcont 17511  prcnt 17519  efilcp 17520  fisub 17522  fbaslim2 17529  limfilnei 17536  conttnf 17537  iscnp3 17539  cnpfillim4 17540  cmptdst 17544  limhun 17546  exopcopn 17548  prdnei 17549  limptlimpr2lem1 17550  limptlimpr2lem2 17551  flimfnei2 17553  islimrs 17556  islimrs3 17557  islimrs4 17558  bwt2 17573  iintlem1 17608  iint 17610  cnvtr 17614  mlteqer 17615  xrletr2 17616  lteqttos 17621  lvsovso 17637  lvsovso3 17639  supnuf 17640  claddrvr 17659  sigadd 17660  addcomv 17666  addcanrg 17678  negveudr 17680  subclrvd 17685  distsava 17700  intvconlem1 17716  hdrmp 17719  cmppfd 17761  domcmpd 17762  codcmpd 17763  cmpasso 17789  cmpida 17790  cmpidb 17791  dualalg 17800  dualded 17801  dualcat2 17802  cmpassoh 17819  homgrf 17820  imonclem 17831  cmpmon 17833  iepiclem 17841  isepic 17842  idfisf 17859  issrc 17885  propsrc 17886  partarelt1 17914  inttaror 17918  inttarcar 17919  fnctartar 17925  fnctartar2 17926  prismorcset2 17937  cmpmor 17994  setiscat 17998  lemindclsbu 18049  indcls2 18050  clscnc 18064  pgapspf2 18107  elicc3 18140  fictb 18145  nn0prpwlem 18152  nn0prpw 18153  2ndcctbss 18205  fnetr 18222  topbasfne 18226  fnessref 18230  neibastop1 18245  neibastop2lem2 18247  neibastop2lem3 18248  neibastop3 18251  topmtcl 18252  fnejoin1 18257  fnejoin2 18258  t0dist 18268  t1sep 18273  regsep 18277  nrmsep 18281  nrmsep2 18282  fmfnfmlem1 18323  flimfbas 18330  fclsfnflim 18343  fcluscomplem 18349  fzmul 18489  fdc 18503  seqpo 18505  incsequz 18506  heibor1lem 18566  ghomco 18608  zerdivemp1x 18621  pridlc 18725  ceqsex3OLD 18755  nelss 18791  domunsncan 18836  xpwdomg 18900  mreiincl 18975  iscldtop 19016  marypha1 19022  fphpd 19138  jm2.19lem3 19359  setindtr 19392  dfac21i 19464  infpssrlem3 19494  fin23lem6 19507  fin56 19597  fin1a2lem6 19605  fin1a2lem10 19609  fin1a2lem12 19611  aalioulem2 19629  islssfg2 19701  mpaaeu 19933  pm14.24 20068  hirstL-ax3 20120  sb5ALT 20167  truniALT 20184  onfrALTlem3 20188  ee223 20261  3orbi123VD 20409  sbc3orgVD 20410  exbirVD 20412  exbiriVD 20413  sbcim2gVD 20434  trsbcVD 20436  truniALTVD 20437  onfrALTlem3VD 20446  onfrALTlem2VD 20448  csbrngVD 20455  19.41rgVD 20461  a9e2eqVD 20466  a9e2ndeqVD 20468  2uasbanhVD 20470  sb5ALTVD 20472  vk15.4jVD 20473  cdleme18d 23334  tendovalco 23804  cdlemn11pre 24249  dihord2pre 24264
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
Copyright terms: Public domain