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 2354  3gencl 2355  rcla4cv 2409  ceqex 2424  mob 2477  euind 2482  reuind 2493  sseq2 2679  uniiunlem 2732  uneqdifeq 2988  difsn 3176  eqsn 3192  preq12b 3203  intab 3297  iinss2 3351  trint0 3468  dtru 3537  sspwb 3556  copsexg 3582  pocl 3646  pofun 3655  solin 3663  frss 3680  fr2nr 3684  efrirr 3687  tz7.7 3731  ordtri3 3741  ordtr2 3749  suc11 3807  onssneli 3813  eusv2 3857  ralxfrALT 3883  iunpw 3904  fr3nr 3905  ordom 3997  peano5 4011  2optocl 4108  3optocl 4109  ssrel 4122  ssrelrel 4131  opeliunxp2 4168  relop 4178  eliniseg2 4361  sotri3 4380  poltletr 4385  xp11 4417  relcnvtr 4480  fss 4624  fv3 4751  tz6.12-1 4754  tz6.12c 4758  tz6.12i 4759  fvopab2 4817  fornex 4873  funfvima 4928  fvclss 4933  f1fveq 4959  isotr 4990  isotrALT 4991  isomin 4992  oprabid 5023  ovg 5091  mpteqb 5225  poxp 5400  soxp 5401  iotaval 5418  smores 5457  smoel 5465  smogt 5472  smoiso2 5474  smoge 5475  tfrlem2 5477  tfrlem9 5485  tfr3 5492  tz7.48-2 5521  tz7.48-3 5523  tz7.49 5524  abianfp 5527  oecl 5577  oaordex 5597  oalimcl 5599  oaass 5600  oarec 5601  omordi 5602  omlimcl 5614  odi 5615  omeulem1 5618  oen0 5621  oewordri 5627  oeworde 5628  oaabs 5664  omsmolem 5668  2ecoptocl 5739  3ecoptocl 5740  eceqoveq 5754  th3qlem2 5756  undifixp 5825  dom3d 5868  xpdom2 5918  infensuc 6048  php 6054  onomeneq 6059  unxpdomlem2 6073  unxpdomlem3 6074  isinf 6083  findcard2 6101  unblem2 6113  unifi 6131  indexfi 6134  finsschain 6152  supub 6183  suplub 6184  supsnALT 6198  ordiso 6199  ordtypelem3 6202  ordtypelem4 6203  ordtypelem6 6205  ordtypelem7 6206  ordtype 6207  hartogs 6209  card2on 6219  card2inf 6220  elirrv 6226  inf3lem1 6244  inf3lem2 6245  inf3lem3 6246  inf3lem5 6248  noinfep 6272  noinfepOLD 6273  trcl 6274  tcel 6293  r1sdom 6304  rankr1c 6344  rankval3b 6347  rankr1 6355  rankel 6361  rankxpsuc 6401  scottex 6404  carddomi2 6444  ondomcard 6452  pr2ne 6470  dif1card 6472  aceq3lem 6503  aceq8clem 6518  fodomnum 6526  cardaleph 6531  cflim2 6629  cfsmolem 6635  domtriomlem 6648  axdc3lem4 6658  axdc4lem 6660  kmlem4 6692  kmlem9 6697  kmlem12 6700  kmlem13 6701  zorn2lem3 6713  zorn2lem4 6714  zorn2lem5 6715  zorn2lem6 6716  zorn2lem7 6717  zornn0 6721  axdclem 6722  axdclem2 6723  ondomon 6758  alephval2 6765  cfpwsdom 6792  axrepnd 6802  tsksdom 6853  tskr1om 6864  grupr 6893  gruiun 6895  ingru 6910  grothomex 6924  indpi 7004  nqereu 7027  genpnnp 7103  prlem934 7131  ltaddpr2 7133  reclem2pr 7146  mulgt0sr 7202  supsrlem 7208  mul0ori 7673  lemul1a 7810  squeeze0 7874  peano5nni 7923  nnunb 8101  fzind 8232  nn0ind-raph 8235  zindd 8236  eluzadd 8297  uzin 8300  icoshft 8607  fzen 8659  fzss1 8677  expcllem 8882  expeq0 8897  mulexp 8906  expword2i 8923  bernneq 8984  facdiv 9016  hashmap 9084  cjexp 9175  absexp 9307  abssubne0 9325  iseraltlem2 9521  sin01gt0 9805  alzdvds 9913  dvdslegcd 9949  gcdneg 9958  rprimelpwr 9987  qredeq 10034  exprmfctlem 10037  prmpwdvds 10154  prmreclem4 10169  imasleval 10478  drsdirfi 10505  pslem 10674  spwmo 10685  ghmnsgima 10919  gxnn0add 11599  gxnn0mul 11602  ismgm 11645  isexid2 11650  rngodm1dm2 11767  rngosn4 11778  fiinopn 11799  tgcl 11844  tgss2 11860  distop 11872  ssnei2 11968  opnnei 11972  tgcnp 12038  cnpnei 12049  cncnplem2 12060  cncmp 12106  cmpfi 12124  2ndcctbss 12172  1stcelcls 12213  cnmptcom 12335  fbfinnfr 12406  isfildlem 12417  snfil 12425  fbunfip 12428  fgfild 12436  fbflim2 12463  elfm2 12483  cnpflf2 12496  meteq0 12517  neibl 12588  reconn 12673  pi1gplem 12804  caubl 12845  ipassi 13184  ubthlem2 13215  minveclem5 13225  volsuplem 13409  dvnadd 13748  dvnres 13749  cpnord 13753  logcnlem1 14163  cxpmul2 14212  qabvexp 14450  isch3 14809  shintcli 14897  shmodsi 14957  spansncvi 15238  pjjsi 15286  hoaddsub 15385  eigorthi 15406  cnlnadjlem5 15639  pjss2coi 15732  pjnormssi 15736  pj3cor1i 15777  strb 15826  dmdmd 15868  mdsl0 15878  csmdsymi 15902  chrelat2i 15933  cvati 15934  mdsymlem3 15973  mdsymlem6 15976  sumdmdlem2 15987  dmdbr5ati 15990  wilthlem3 16132  3ccased 16687  dedekind 16693  dfres3 16731  dfon2lem3 16760  omssadd 16773  rdgprc 16782  trpredmintr 16869  trpredrec 16876  wfr3g 16890  wfrlem12 16902  frr3g 16915  frrlem11 16928  sltval2 16944  axfelem13 16993  elfuns 17095  axcontlem4 17233  cgrextend 17269  btwndiff 17288  btwnconn1lem12 17359  brsegle 17369  broutsideof2 17383  funray 17401  meran1 17563  waj-ax 17566  arg-ax 17568  wl-pm2.86i 17611  copsexgb 17650  evpexun 17679  cpref 17732  inttr 17737  isunscov 17739  restidsing 17741  twsymr 17743  prj1b 17744  prj3 17745  set2elt 17757  fixpc 17766  elovdm2 17799  domintrefc 17800  mapmapmap 17825  injsurinj 17826  repfuntw 17838  repcpwti 17839  cbcpcp 17840  prl 17845  prl2 17847  prjmapcp2 17848  dstr 17849  nZdef 17858  jidd 17870  midd 17871  preotr2 17913  int2pre 17915  ubpar 17941  inposet 17958  tolat 17969  pospos 17973  toplat 17976  latdir 17981  ridlideq 18021  rzrlzreq 18022  resgcom 18037  grpodivone 18059  grpodivfo 18060  rltrran 18101  zerdivemp1 18123  zintdom 18125  muldisc 18171  svli2 18174  svs2 18177  truni1 18195  truni2 18196  truni3 18197  inttop2 18216  npmp 18222  mapudiscn 18229  nsn 18231  top2ind 18255  top2usne 18256  homindlem3 18258  intopcoaconlem3b 18259  intopcoaconc 18262  qusp 18263  intcont 18264  prcnt 18272  efilcp 18273  fisub 18275  iscnp3 18287  cmptdst 18292  exopcopn 18296  prdnei 18297  limptlimpr2lem1 18298  limptlimpr2lem2 18299  flfnei2 18301  islimrs 18304  islimrs3 18305  islimrs4 18306  bwt2 18319  iintlem1 18352  iint 18354  cnvtr 18358  mlteqer 18359  xrletr2 18360  lteqttos 18365  lvsovso 18381  lvsovso3 18383  supnuf 18384  claddrvr 18403  sigadd 18404  addcomv 18410  addcanrg 18422  negveudr 18424  subclrvd 18429  distsava 18444  intvconlem1 18460  hdrmp 18463  cmppfd 18502  domcmpd 18503  codcmpd 18504  cmpasso 18530  cmpida 18531  cmpidb 18532  dualalg 18541  dualded 18542  dualcat2 18543  cmpassoh 18560  homgrf 18561  imonclem 18572  cmpmon 18574  iepiclem 18582  isepic 18583  idfisf 18600  issrc 18626  propsrc 18627  partarelt1 18655  inttaror 18659  inttarcar 18660  fnctartar 18666  fnctartar2 18667  prismorcset2 18678  cmpmor 18735  setiscat 18739  lemindclsbu 18790  indcls2 18791  clscnc 18805  pgapspf2 18848  elicc3 18881  nn0prpwlem 18891  nn0prpw 18892  fnetr 18945  topbasfne 18949  fnessref 18953  neibastop1 18968  neibastop2lem2 18970  neibastop2lem3 18971  neibastop3 18974  topmtcl 18975  fnejoin1 18980  fnejoin2 18981  t0dist 18991  t1sep 18996  regsep 19000  nrmsep 19004  nrmsep2 19005  fmfnfmlem1 19040  flimfbas 19047  flimfcls 19064  filnetlem4 19091  fzmul 19208  fdc 19222  seqpo 19224  incsequz 19225  heibor1lem 19285  ghomco 19327  zerdivemp1x 19340  pridlc 19444  ceqsex3OLD 19474  nelss 19510  domunsncan 19554  xpwdomg 19614  mreiincl 19689  iscldtop 19730  marypha1 19736  fphpd 19852  jm2.19lem3 20072  setindtr 20105  dfac21i 20175  infpssrlem3 20203  fin23lem6 20216  fin56 20306  fin1a2lem6 20314  fin1a2lem10 20318  fin1a2lem12 20320  aalioulem2 20338  islssfg2 20410  mpaaeu 20639  pm14.24 20774  hirstL-ax3 20826  sb5ALT 20873  truniALT 20890  onfrALTlem3 20894  ee223 20984  3orbi123VD 21135  sbc3orgVD 21136  exbirVD 21138  exbiriVD 21139  sbcim2gVD 21160  trsbcVD 21162  truniALTVD 21163  onfrALTlem3VD 21172  onfrALTlem2VD 21174  csbrngVD 21181  19.41rgVD 21187  a9e2eqVD 21192  a9e2ndeqVD 21194  2uasbanhVD 21196  sb5ALTVD 21201  vk15.4jVD 21202  cdleme18d 24070  tendovalco 24540  cdlemn11pre 24986  dihord2pre 25001
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
Copyright terms: Public domain