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 19 . 2 |- (ps -> ps)
2 com12.1 . 2 |- (ph -> (ps -> ch))
31, 2syl5com 27 1 |- (ps -> (ph -> ch))
Colors of variables: wff set class
Syntax hints:   -> wi 4
This theorem is referenced by:  syl5 29  syl6com 32  mpcom 33  syli 34  pm2.27 36  pm2.43b 48  syl9r 69  com3r 75  pm2.86i 94  pm2.24 102  con3rr3 128  expt 148  jad 156  pm2.61dOLD 159  pm2.61 167  pm2.6OLD 169  biimpcdOLD 216  syl5ibcom 229  syl5ibrcom 231  biimprcdOLD 235  pm5.501 350  jaod 393  orel1 394  pm2.62 423  pm2.621OLD 427  impcom 444  imp3a 445  expcom 449  exp3a 450  pm3.21 457  anim12iiOLD 578  imdistanri 699  pm2.64 762  pm2.75 824  ccased 924  dedlem0b 930  3impd 1171  3expd 1174  mp3an1i 1275  meredith 1291  simplbi2com 1371  a9wa9lem2 1476  a9wa9lem2OLD 1477  a9wa9lem6OLD 1482  hbimd 1575  19.21t 1578  equtrr 1595  sbequ2 1640  ax11b 1683  sb6rf 1725  sb56 1731  exmoeu 1893  moimv 1899  eupickbi 1917  2eu1 1931  exists2 1941  r19.12 2272  2gencl 2393  3gencl 2394  rcla4cv 2448  ceqex 2463  euind 2519  reuind 2530  sseq2 2705  uniiunlem 2757  disjne 2969  uneqdifeq 3004  difsn 3181  eqsn 3196  preq12b 3205  intab 3294  iinss2 3347  trint0 3461  dtru 3530  sspwb 3549  pocl 3636  pofun 3645  solin 3653  frss 3669  fr2nr 3673  efrirr 3676  tz7.7 3720  ordtri3 3730  ordtr2 3738  suc11 3795  onssneli 3801  eusv2 3845  ralxfr 3866  iunpw 3885  fr3nr 3886  ordom 3976  peano5 3990  2optocl 4086  3optocl 4087  ssrel 4100  ssrelrel 4109  relop 4144  sotri3 4338  xp11 4368  relcnvtr 4430  fss 4573  fv3 4690  tz6.12-1 4693  tz6.12c 4697  tz6.12i 4698  fvco2 4736  fvopab2 4753  fornex 4802  funfvima 4857  fvclss 4861  f1fveq 4887  isotr 4912  isotrALT 4913  isomin 4914  oprabid 4945  ovg 5009  poxp 5227  soxp 5228  iotaval 5245  smores 5279  smoel 5287  smogt 5294  smoiso2 5296  smoge 5297  tfrlem2 5299  tfrlem9 5307  tfr3 5314  tz7.48-2 5343  tz7.48-3 5345  tz7.49 5346  abianfp 5349  oecl 5398  oaordex 5418  oalimcl 5420  oaass 5421  oarec 5422  omordi 5423  omlimcl 5435  odi 5436  omeulem1 5439  oen0 5442  oewordri 5448  oeworde 5449  oaabs 5485  omsmolem 5489  2ecoptocl 5556  3ecoptocl 5557  eceqoveq 5571  th3qlem2 5573  dom3d 5677  xpdom2 5721  infensuc 5843  php 5849  onomeneq 5854  unxpdomlem2 5868  unxpdomlem3 5869  isinf 5878  domfi 5887  findcard 5894  findcard2 5895  unblem2 5906  unifi 5924  indexfi 5927  supub 5968  suplub 5969  supsnALT 5982  ordiso 5983  ordtypelem3 5986  ordtypelem4 5987  ordtypelem6 5989  ordtypelem7 5990  ordtype 5991  hartogs 5993  card2on 5996  card2inf 5997  elirrv 6003  inf3lem1 6021  inf3lem2 6022  inf3lem3 6023  inf3lem5 6025  noinfep 6049  noinfepOLD 6050  trcl 6051  tcel 6071  r1sdom 6082  rankr1c 6122  rankval3b 6125  rankr1 6133  rankel 6139  rankxpsuc 6179  scottex 6182  carddomi2 6222  ondomcard 6230  pr2ne 6245  dif1card 6247  omsubsdomlem2 6274  elomsubsd 6279  infenomsub 6283  aceq3lem 6289  aceq8clem 6304  fodomnum 6312  cardaleph 6317  cflim2 6386  cfsmolem 6392  domtriomlem 6405  axdc3lem4 6415  axdc4lem 6417  kmlem4 6449  kmlem9 6454  kmlem12 6457  kmlem13 6458  numthlem 6464  zorn2lem3 6471  zorn2lem4 6472  zorn2lem5 6473  zorn2lem6 6474  zorn2lem7 6475  zornn0 6479  axdclem 6480  axdclem2 6481  ondomon 6516  alephval2 6523  cfpwsdom 6550  axrepnd 6560  tsksdom 6614  tskssel2 6615  tsk2 6621  tskr1om 6623  grupr 6648  gruiun 6650  ingru 6665  grothomex 6679  indpi 6752  nqereu 6775  genpnnp 6851  prlem934 6879  ltaddpr2 6881  reclem2pr 6894  mulgt0sr 6950  supsrlem 6956  mul0ori 7417  lemul1a 7552  squeeze0 7616  peano5nni 7662  nnunb 7826  fzind 7956  nn0ind-raph 7959  zindd 7960  eluzadd 8019  uzin 8022  suprzcl 8069  ico0 8272  ioc0 8273  iccss2 8288  icoshft 8319  fzen 8369  fzss1 8386  expcllem 8583  expeq0 8597  mulexp 8606  expword2i 8623  bernneq 8685  facdiv 8716  cjexp 8862  sqrmo 8918  absexp 8992  abssubne0 9007  caurcvg 9123  sin01gt0 9419  alzdvds 9523  dvdslegcd 9557  gcdneg 9566  rprimelpwr 9595  exprmfctlem 9642  prmpwdvds 9745  pslem 10030  spwmo 10041  gxnn0add 10484  gxnn0mul 10487  ismgm 10536  isexid2 10541  grpomnd 10562  isga 10592  ssga 10597  gagrpid 10600  gaass 10601  gapmlem 10603  rngodm1dm2 10656  rngosn4 10667  fiinopn 10697  tgcl 10741  tgss2 10755  distop 10766  ssnei2 10855  opnnei 10859  cnpnei 10909  cnpco 10912  cncnplem2 10918  cncmp 10943  cmpfi 10955  usinuniop 10960  dfcon2 10961  cnmptcom 10999  fbfinnfr 11027  isfildlem 11037  snfil 11045  fbunfip 11048  fgfild 11056  limfilss 11068  elfm2 11083  flimopn 11090  meteq0 11115  neibl 11186  metequivlem 11194  reconn 11259  iccconn 11261  pi1gplem 11345  caubl 11403  ipassi 11743  ubthlem2 11774  minveclem5 11784  isch3 12283  shintcli 12371  shmodsi 12431  spansncvi 12712  pjjsi 12760  hoaddsub 12859  eigorthi 12880  homco2 13019  cnlnadjlem5 13113  pjss2coi 13206  pjnormssi 13210  pj3cor1i 13251  strb 13300  dmdmd 13342  mdsl0 13352  csmdsymi 13376  chrelat2i 13407  cvati 13408  mdsymlem3 13447  mdsymlem6 13450  sumdmdlem2 13461  dmdbr5ati 13464  volsuplem 13681  3ccased 13914  dedekind 13921  dfres3 13964  dfon2lem3 13994  omssadd 14007  rdgprc 14016  trpredmintr 14103  trpredrec 14110  wfr3g 14124  wfrlem12 14136  frr3g 14149  frrlem11 14162  sltval2 14178  axfelem13 14227  elfuns 14329  axcontlem4 14467  cgrextend 14503  btwndiff 14522  btwnconn1lem12 14593  brsegle 14603  broutsideof2 14617  funray 14635  meran1 14797  waj-ax 14800  arg-ax 14802  wl-pm2.86i 14845  copsexgb 14885  evpexun 14913  cpref 14967  inttr 14972  isunscov 14974  restidsing 14978  twsymr 14981  prj1b 14982  prj3 14983  set2elt 14995  fixpc 15004  surjsec 15034  injrec2 15035  surjsec2 15036  elovdm2 15044  domintrefc 15045  elico3 15062  elioc3 15063  mapmapmap 15072  injsurinj 15073  repfuntw 15085  repcpwti 15086  cbcpcp 15087  unprj 15092  prl 15093  prl2 15095  prjmapcp2 15096  dstr 15097  nZdef 15106  jidd 15118  midd 15119  preotr2 15153  int2pre 15155  ubpar 15181  inposet 15198  tolat 15209  pospos 15213  toplat 15216  latdir 15221  ridlideq 15263  rzrlzreq 15264  resgcom 15280  symgfo 15298  curgrpact 15303  grpodivone 15304  grpodivfo 15305  cmprltr 15345  rltrran 15349  zerdivemp1 15371  zintdom 15373  muldisc 15415  svli2 15418  svs2 15421  truni1 15439  truni2 15440  truni3 15441  inttop2 15450  npmp 15456  mapdiscnlem 15463  mapdiscn 15464  mapudiscn 15465  nsn 15467  top2ind 15492  top2usne 15493  homindlem3 15495  intopcoaconlem3b 15496  intopcoaconc 15499  qusp 15500  intcont 15501  prtoptop 15507  prcnt 15509  efilcp 15510  fisub 15512  fbaslim2 15519  limfilnei 15526  conttnf 15527  iscnp3 15529  cnpfillim4 15530  cmptdst 15534  limhun 15536  exopcopn 15538  prdnei 15539  limptlimpr2lem1 15540  limptlimpr2lem2 15541  flimfnei2 15543  islimrs 15546  islimrs3 15547  islimrs4 15548  bwt2 15563  grpohmlem1 15588  grpohmlem2 15589  grpohlem3 15590  grpohmlem4 15591  grpohlem5 15592  grpohm 15593  iintlem1 15613  iint 15615  cnvtr 15619  mlteqer 15620  xrletr2 15621  lteqtpos 15627  lvsovso 15643  lvsovso3 15645  supnuf 15646  claddrvr 15665  sigadd 15666  addcomv 15672  cnegvex2 15677  addcanri 15683  addcanrg 15684  negveud 15685  negveudr 15686  issubcv 15687  subaddv 15688  subclrvd 15691  distsava 15706  intvconlem1 15722  consuba 15725  hdrmp 15728  cmppfd 15770  domcmpd 15771  codcmpd 15772  cmpasso 15798  cmpida 15799  cmpidb 15800  dualalg 15809  dualded 15810  dualcat2 15811  cmpassoh 15828  homgrf 15829  imonclem 15840  cmpmon 15842  iepiclem 15850  isepic 15851  idfisf 15867  propsrc 15892  tartrel 15912  tartord 15913  cptarc 15915  sexptrt 15916  tarsuc2 15918  bpmp 15924  btmp 15925  intartar 15928  tartarmap 15938  vtarsuelt 15945  partarelt1 15946  inttaror 15950  inttarcar 15951  cartarlim 15955  fnctartar 15957  fnctartar2 15958  prismorcset2 15969  morexcmp 16018  cmpmor 16026  setiscat 16030  lemindclsbu 16081  indcls2 16082  clscnc 16096  pgapspf2 16139  elicc3 16172  fictb 16179  finsschain 16180  nn0prpwlem 16188  nn0prpw 16189  qredeq 16190  2ndcctbss 16252  fnetr 16269  topbasfne 16273  fnessref 16277  neibastop1 16292  neibastop2lem2 16294  neibastop2lem3 16295  neibastop3 16298  topmtcl 16299  fnejoin1 16304  fnejoin2 16305  t0dist 16315  t1sep 16320  regsep 16324  nrmsep 16328  nrmsep2 16329  fmfnfmlem1 16370  flimfbas 16377  fclsfnflim 16390  fcluscomplem 16396  fzmul 16538  fdc 16553  seqpo 16555  incsequz 16556  heibor1lem 16617  ghomco 16659  zerdivemp1x 16672  pridlc 16782  ceqsex3OLD 16812  pm14.24 16947  sb5ALT 17045  truniALT 17062  onfrALTlem3 17066  ee223 17138  3orbi123VD 17286  sbc3orgVD 17287  exbirVD 17289  exbiriVD 17290  sbcim2gVD 17311  trsbcVD 17313  truniALTVD 17314  onfrALTlem3VD 17323  onfrALTlem2VD 17325  csbrngVD 17332  19.41rgVD 17338  a9e2eqVD 17343  a9e2ndeqVD 17345  2uasbanhVD 17347  sb5ALTVD 17348  vk15.4jVD 17349  pexmidALT 19721  cdleme18d 20094  tendovalco 20587  cdlemn11pre 21024  dihord2pre 21039
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
Copyright terms: Public domain