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

Theorem com12 28
Description: Inference that swaps (commutes) antecedents in an implication. (The proof was shortened by Wolf Lammen, 4-Aug-2012.)
Hypothesis
Ref Expression
com12.1 |- (ph -> (ps -> ch))
Assertion
Ref Expression
com12 |- (ps -> (ph -> ch))

Proof of Theorem com12
StepHypRef Expression
1 id 18 . 2 |- (ps -> ps)
2 com12.1 . 2 |- (ph -> (ps -> ch))
31, 2syl5com 26 1 |- (ps -> (ph -> ch))
Colors of variables: wff set class
Syntax hints:   -> wi 3
This theorem is referenced by:  syl5 29  syl6com 32  mpcom 33  syli 34  pm2.27 36  pm2.43b 48  syl9r 72  imim1OLD 76  com3r 81  pm2.86i 100  pm2.24 111  con3rr3 144  expt 165  jad 173  pm2.61dOLD 176  pm2.61 185  pm2.6OLD 187  biimpcdOLD 236  syl5ibcom 251  syl5ibrcom 255  biimprcdOLD 261  pm5.501 385  jaod 429  orel1 430  orel2OLD 432  pm2.62 460  pm2.621OLD 464  impcom 481  imp3a 482  expcom 486  exp3a 487  pm3.21 499  anim12iiOLD 641  imdistanri 782  pm2.64 850  pm2.75 911  ccased 1014  dedlem0aOLD 1020  dedlem0b 1021  3impd 1260  3expd 1263  mp3an1i 1388  meredith 1404  simplbi2com 1503  a9wa9lem2 1611  a9wa9lem6 1615  hbimd 1707  19.21t 1710  equtrr 1727  sbequ2 1772  ax11b 1815  sb6rf 1857  sb56 1863  exmoeu 2025  moimv 2031  eupickbi 2049  2eu1 2063  exists2 2073  r19.12 2409  2gencl 2528  2genclOLD 2529  3gencl 2530  3genclOLD 2531  rcla4cv 2588  ceqex 2602  euind 2658  reuind 2669  sseq2 2842  uniiunlem 2896  disjne 3107  uneqdifeq 3142  difsn 3315  eqsn 3330  preq12b 3339  intab 3427  iinss2 3480  trint0 3598  dtru 3668  sspwb 3687  pocl 3774  pofun 3781  solin 3789  frss 3804  fr2nr 3808  efrirr 3811  tz7.7 3855  ordtri3 3865  ordtr2 3873  suc11 3931  onssneli 3937  eusv2OLD 3981  eusv2 3982  ralxfr 4003  iunpw 4022  fr3nr 4023  ordom 4113  peano5 4127  2optocl 4219  3optocl 4220  ssrel 4233  ssrelrel 4242  relop 4278  sotri3 4471  xp11 4499  relcnvtr 4563  fss 4714  fv3 4831  tz6.12-1 4834  tz6.12c 4838  tz6.12i 4839  fvco2 4876  fvopab2 4893  fornex 4941  funfvima 5002  fvclss 5006  f1fveq 5031  isotr 5056  isotrALT 5057  isomin 5058  oprabid 5088  poxp 5367  soxp 5368  iotaval 5385  smores 5419  smoel 5427  smogt 5434  smoiso2 5436  smoge 5437  tfrlem2 5439  tfrlem9 5447  tfr3 5454  tz7.48-2 5483  tz7.48-2OLD 5484  tz7.48-3 5486  tz7.49OLD 5487  tz7.49 5489  abianfp 5492  oecl 5541  oaordex 5561  oalimcl 5563  oaass 5564  oarec 5565  omordi 5566  omlimcl 5578  odi 5579  omeulem1 5582  oen0 5585  oewordri 5591  oeworde 5592  oaabs 5628  omsmolem 5632  2ecoptocl 5685  3ecoptocl 5686  eceqopreq 5694  th3qlem2 5696  dom3d 5791  xpdom2 5835  infensuc 5960  php 5966  onomeneq 5971  unxpdomlem2 5985  unxpdomlem3 5986  isinf 5995  domfi 6004  findcard 6012  findcard2 6013  unblem2 6024  unifi 6042  indexfi 6045  supub 6072  suplub 6073  supsnALT 6086  ordiso 6087  ordtypelem3 6090  ordtypelem4 6091  ordtypelem6 6093  ordtypelem7 6094  ordtype 6095  hartogs 6097  card2on 6100  card2inf 6101  elirrv 6107  inf3lem1 6125  inf3lem2 6126  inf3lem3 6127  inf3lem5 6129  noinfep 6155  noinfepOLD 6156  trcl 6157  tcel 6178  r1sdom 6189  rankr1c 6233  rankelbOLD 6236  rankval3b 6237  rankr1 6246  rankel 6252  rankxpsuc 6293  truniALT 6307  onfrALTlem3 6311  scottex 6328  carddomi2 6368  ondomcard 6376  pr2ne 6391  dif1card 6393  dif1cardOLD 6394  omsubsdomlem2 6421  elomsubsd 6426  infenomsub 6430  aceq3lem 6436  aceq8clem 6451  fodomnum 6459  cardaleph 6464  cflim2 6533  cfsmolem 6539  domtriomlem 6552  axdc3lem4 6562  axdc4lem 6564  kmlem4 6596  kmlem9 6601  kmlem12 6604  kmlem13 6605  numthlem 6611  zorn2lem3 6618  zorn2lem4 6619  zorn2lem5 6620  zorn2lem6 6621  zorn2lem7 6622  zornn0 6626  axdclem 6627  axdclem2 6628  ondomon 6663  alephval2 6670  cfpwsdom 6697  tsksdom 6727  tskssel2 6728  tsk2 6734  tskr1om 6736  grupr 6761  gruiun 6763  ingru 6778  grothomex 6792  axrepnd 6807  indpi 6898  nqereu 6921  genpnnp 6997  prlem934 7025  ltaddpr2 7027  reclem2pr 7040  mulgt0sr 7096  supsrlem 7102  mul0ori 7555  lemul1a 7693  squeeze0 7768  nnunb 8001  dfuzi 8116  fzind 8129  nn0ind-raph 8132  zindd 8133  uzwo3lem1 8135  eluzadd 8168  uzin 8171  suprzcl 8216  monoord 8397  icoshft 8461  fzen 8500  fzss1 8517  seqf2 8603  seqfveq2 8605  serf1o 8619  seq1rn2 8650  seqzrn2 8704  expcllem 8726  expeq0 8736  expgt0 8739  expgt1 8742  mulexp 8744  exprec 8745  exprecOLD 8746  bernneq 8813  bernneqOLD 8814  cjexp 8906  sqrmo 8943  absexp 9016  abssubne0 9031  cvg2i 9071  facdiv 9106  fseq1hash 9150  fsumrev 9218  2climnn 9297  2climnn0 9298  iserzmulc1 9333  caucvglem6 9359  caucvgi 9360  cvgratlem1 9449  cvgratlem2 9450  sin01bndlem2 9680  cos01bndlem2 9682  sin01gt0 9688  alzdvds 9816  dvdslegcd 9846  gcdneg 9855  mulgcdlem2 9882  exprmfctlem 9910  1arithlem22 9947  1arithlem30 9956  lmodlema 10275  tgcl 10438  tgss2 10451  subbas2 10459  distop 10463  ssnei2 10567  opnnei 10571  cnpnei 10620  cnpco 10623  cncnplem2 10629  meteq0 10661  neibl 10729  metequivlem 10737  caun0 10805  caubl 10829  xplmi 10836  lmcau 10859  gxnn0add 10957  gxnn0mul 10960  isga 11012  ssga 11017  gagrpid 11020  gaass 11021  gapmlem 11023  vacnlem3 11229  vacnlem6 11232  ipassi 11397  ubthlem2 11428  pslem 11521  spwmo 11529  efifolem5 11606  hmeobc 11721  cnvhmpha 11722  fbfinnfr 11738  isfildlem 11748  snfil 11756  fbunfip 11759  fgfild 11767  limfilss 11778  elfm2 11793  flimopn 11800  cncomp 11810  usinuniop 11820  ismgm 11848  isexid2 11853  grpmnd 11874  rnplrnml0 11883  on1el4 11894  isch3 12224  projlem28 12323  projlem29 12324  pjthlem14 12342  shintcli 12404  shmodsi 12471  spansni 12589  spansncvi 12706  pjjsi 12754  hoaddsub 12853  eigorthi 12874  homco2 13011  cnlnadjlem5 13103  pjss2coi 13197  pjnormssi 13201  pj3cor1i 13243  strb 13292  dmdmd 13334  mdsl0 13344  csmdsymi 13368  chrelat2i 13399  cvati 13400  mdsymlem3 13439  mdsymlem6 13442  sumdmdlem2 13453  dmdbr5ati 13456  nqereuNEW 13495  fsumlem 13551  isummulc1NEW 13572  isumdivcNEW 13574  dfuziNEW 13586  prmpwdvds 13680  fseq1cl 13931  dedekind 13982  dfon2lem3 14043  omssadd 14056  trpredmintr 14142  trpredrec 14149  wfr3g 14163  wfrlem12 14175  frr3g 14188  frrlem11 14201  sltval2 14217  axfelem13 14266  elfuns 14329  axcontlem4 14436  cgrextend 14472  btwndiff 14490  btwnconn1lem12 14544  brsegle 14553  meran1 14694  waj-ax 14697  arg-ax 14699  wl-pm2.86i 14742  coprsexg 14783  evpexun 14809  uninqs 14827  cpref 14863  inttr 14868  isunscov 14870  restidsing 14874  twsymr 14877  prj1b 14878  prj3 14879  set2elt 14891  fixpc 14901  surjsec 14931  injrec2 14932  surjsec2 14933  eloprvdm2 14942  domintrefc 14943  mapmapmap 14970  injsurinj 14971  prmapcp2 14982  npincppr 14986  repfuntw 14987  repcpwti 14988  cbcpcp 14989  prjmapcp 14992  cbicplem 14993  unprj 14996  prl 14997  prl2 14999  prjmapcp2 15000  dstr 15001  nZdef 15010  jidd 15025  midd 15026  preotr2 15061  int2pre 15063  ubpar 15088  inposet 15105  tolat 15116  pospos 15120  toplat 15123  latdir 15128  fprod1ib 15171  ridlideq 15176  rzrlzreq 15177  clfsebs 15188  resgcom 15193  symgfo 15211  curgrpact 15216  grpdivone 15217  grpdivfo 15218  cmprltr 15258  rltrran 15262  zerdivemp1 15284  zintdom 15286  muldisc 15330  svli2 15332  svs2 15335  truni1 15355  truni2 15356  truni3 15357  inttop2 15366  neffopo 15371  npmp 15374  mapdiscnlem 15381  mapdiscn 15382  mapudiscn 15383  nsn 15385  cnvhmphb 15391  hmphre 15395  hmeogrp 15403  homcard 15404  top2ind 15408  top2usne 15409  homindlem3 15411  intopcoaconlem3b 15412  intopcoaconc 15415  qusp 15416  intcont 15420  prtoptop 15426  prcnt 15428  efilcp 15429  fisub 15431  fbaslim2 15438  limfilnei 15445  conttnf 15446  iscnp3 15448  cnpfillim4 15449  cmptdst 15453  limhun 15455  exopcopn 15457  prdnei 15458  limptlimpr2lem1 15459  limptlimpr2lem2 15460  flimfnei2 15462  islimrs 15465  islimrs3 15466  islimrs4 15467  bwt2 15484  grphmlem1 15509  grphmlem2 15510  grphlem3 15511  grphmlem4 15512  grphlem5 15513  grphm 15514  cntrsetlem 15526  iintlem1 15535  iint 15537  cnvtr 15541  mlteqer 15542  xrletr2 15543  lteqtpos 15549  lvsovso 15565  lvsovso3 15567  supnuf 15568  addcomv 15587  addidv2 15589  cnegvex2 15591  addcanri 15595  addcanrg 15596  negveud 15597  issubcv 15598  cmppfd 15651  domcmpd 15652  codcmpd 15653  cmpasso 15679  cmpida 15680  cmpidb 15681  dualalg 15690  dualded 15691  dualcat2 15692  cmpassoh 15709  homgrf 15710  imonclem 15721  cmpmon 15723  iepiclem 15731  isepic 15732  idfisf 15748  tartrel 15792  tartord 15793  cptarc 15795  sexptrt 15796  tarsuc2 15798  bpmp 15804  btmp 15805  intartar 15808  tartarmap 15818  vtarsuelt 15825  partarelt1 15826  inttaror 15830  inttarcar 15831  cartarlim 15835  fnctartar 15837  fnctartar2 15838  prismorcset2 15849  morexcmp 15898  cmpmor 15906  setiscat 15910  lemindclsbu 15961  indcls2 15962  indclsbusuc 15967  clscnc 15980  pgapspf2 16023  elicc3 16056  dfnn3 16059  fictb 16064  finsschain 16065  nn0prpwlem 16074  nn0prpw 16075  qredeq 16076  compfipin0 16111  dfcon2 16117  reconn 16126  iccconn 16128  2ndcctbss 16153  fnetr 16170  topbasfne 16174  fnessref 16178  neibastop1 16193  neibastop2lem2 16195  neibastop2lem3 16196  neibastop3 16199  topmtcl 16200  fnejoin1 16205  fnejoin2 16206  t0dist 16216  t1sep 16221  regsep 16225  nrmsep 16229  nrmsep2 16230  fmfnfmlem1 16271  flimfbas 16278  fclsfnflim 16291  fcluscomplem 16297  oprabvalg 16381  eropreu 16406  fzmul 16457  sdclem1 16474  sdclem2 16475  sdc 16476  fdc 16477  seqpo 16479  incsequz 16480  iccss2 16520  heibor1lem 16620  ghomco 16675  pcohtpy 16718  zerdivemp1x 16742  pridlc 16852  ceqsex3OLD 16882  pm14.24 17019  sb5ALT 17094  ee223 17150  3orbi123VD 17298  sbc3orgVD 17299  exbirVD 17301  exbiriVD 17302  sbcim2gVD 17323  trsbcVD 17325  truniALTVD 17326  onfrALTlem3VD 17335  onfrALTlem2VD 17337  csbrngVD 17344  19.41rgVD 17350  a9e2eqVD 17355  a9e2ndeqVD 17357  sb5ALTVD 17358  vk15.4jVD 17359  pexmidALT 19738  cdleme18d 20098  tendovalco 20591  cdlemn11pre 21026  dihord2pre 21041
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7
Copyright terms: Public domain