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 7954  nn0ind-raph 7957  zindd 7958  eluzadd 8017  uzin 8020  suprzcl 8067  ico0 8268  ioc0 8269  iccss2 8284  icoshft 8315  fzen 8365  fzss1 8382  expcllem 8578  expeq0 8592  mulexp 8601  expword2i 8618  bernneq 8680  facdiv 8711  cjexp 8857  sqrmo 8913  absexp 8987  abssubne0 9002  caurcvg 9118  sin01gt0 9409  alzdvds 9513  dvdslegcd 9547  gcdneg 9556  rprimelpwr 9585  exprmfctlem 9632  prmpwdvds 9735  pslem 10020  spwmo 10031  gxnn0add 10479  gxnn0mul 10482  ismgm 10531  isexid2 10536  grpomnd 10557  isga 10587  ssga 10592  gagrpid 10595  gaass 10596  gapmlem 10598  rngodm1dm2 10651  rngosn4 10662  fiinopn 10692  tgcl 10736  tgss2 10750  distop 10761  ssnei2 10850  opnnei 10854  cnpnei 10904  cnpco 10907  cncnplem2 10913  cncmp 10938  cmpfi 10950  usinuniop 10955  dfcon2 10956  cnmptcom 10994  fbfinnfr 11022  isfildlem 11032  snfil 11040  fbunfip 11043  fgfild 11051  limfilss 11063  elfm2 11078  flimopn 11085  meteq0 11110  neibl 11181  metequivlem 11189  reconn 11254  iccconn 11256  pi1gplem 11340  caubl 11398  ipassi 11738  ubthlem2 11769  minveclem5 11779  isch3 12278  shintcli 12366  shmodsi 12426  spansncvi 12707  pjjsi 12755  hoaddsub 12854  eigorthi 12875  homco2 13014  cnlnadjlem5 13108  pjss2coi 13201  pjnormssi 13205  pj3cor1i 13246  strb 13295  dmdmd 13337  mdsl0 13347  csmdsymi 13371  chrelat2i 13402  cvati 13403  mdsymlem3 13442  mdsymlem6 13445  sumdmdlem2 13456  dmdbr5ati 13459  volsuplem 13603  3ccased 13836  dedekind 13843  dfres3 13886  dfon2lem3 13916  omssadd 13929  rdgprc 13938  trpredmintr 14025  trpredrec 14032  wfr3g 14046  wfrlem12 14058  frr3g 14071  frrlem11 14084  sltval2 14100  axfelem13 14149  elfuns 14251  axcontlem4 14389  cgrextend 14425  btwndiff 14444  btwnconn1lem12 14515  brsegle 14525  broutsideof2 14539  funray 14557  meran1 14719  waj-ax 14722  arg-ax 14724  wl-pm2.86i 14767  copsexgb 14807  evpexun 14835  cpref 14889  inttr 14894  isunscov 14896  restidsing 14900  twsymr 14903  prj1b 14904  prj3 14905  set2elt 14917  fixpc 14926  surjsec 14956  injrec2 14957  surjsec2 14958  elovdm2 14966  domintrefc 14967  elico3 14984  elioc3 14985  mapmapmap 14994  injsurinj 14995  repfuntw 15007  repcpwti 15008  cbcpcp 15009  unprj 15014  prl 15015  prl2 15017  prjmapcp2 15018  dstr 15019  nZdef 15028  jidd 15040  midd 15041  preotr2 15075  int2pre 15077  ubpar 15103  inposet 15120  tolat 15131  pospos 15135  toplat 15138  latdir 15143  ridlideq 15185  rzrlzreq 15186  resgcom 15202  symgfo 15220  curgrpact 15225  grpodivone 15226  grpodivfo 15227  cmprltr 15267  rltrran 15271  zerdivemp1 15293  zintdom 15295  muldisc 15337  svli2 15340  svs2 15343  truni1 15361  truni2 15362  truni3 15363  inttop2 15372  npmp 15378  mapdiscnlem 15385  mapdiscn 15386  mapudiscn 15387  nsn 15389  top2ind 15414  top2usne 15415  homindlem3 15417  intopcoaconlem3b 15418  intopcoaconc 15421  qusp 15422  intcont 15423  prtoptop 15429  prcnt 15431  efilcp 15432  fisub 15434  fbaslim2 15441  limfilnei 15448  conttnf 15449  iscnp3 15451  cnpfillim4 15452  cmptdst 15456  limhun 15458  exopcopn 15460  prdnei 15461  limptlimpr2lem1 15462  limptlimpr2lem2 15463  flimfnei2 15465  islimrs 15468  islimrs3 15469  islimrs4 15470  bwt2 15485  grpohmlem1 15510  grpohmlem2 15511  grpohlem3 15512  grpohmlem4 15513  grpohlem5 15514  grpohm 15515  iintlem1 15535  iint 15537  cnvtr 15541  mlteqer 15542  xrletr2 15543  lteqtpos 15549  lvsovso 15565  lvsovso3 15567  supnuf 15568  claddrvr 15587  sigadd 15588  addcomv 15594  cnegvex2 15599  addcanri 15605  addcanrg 15606  negveud 15607  negveudr 15608  issubcv 15609  subaddv 15610  subclrvd 15613  distsava 15628  intvconlem1 15644  consuba 15647  hdrmp 15650  cmppfd 15692  domcmpd 15693  codcmpd 15694  cmpasso 15720  cmpida 15721  cmpidb 15722  dualalg 15731  dualded 15732  dualcat2 15733  cmpassoh 15750  homgrf 15751  imonclem 15762  cmpmon 15764  iepiclem 15772  isepic 15773  idfisf 15789  propsrc 15814  tartrel 15834  tartord 15835  cptarc 15837  sexptrt 15838  tarsuc2 15840  bpmp 15846  btmp 15847  intartar 15850  tartarmap 15860  vtarsuelt 15867  partarelt1 15868  inttaror 15872  inttarcar 15873  cartarlim 15877  fnctartar 15879  fnctartar2 15880  prismorcset2 15891  morexcmp 15940  cmpmor 15948  setiscat 15952  lemindclsbu 16003  indcls2 16004  clscnc 16018  pgapspf2 16061  elicc3 16094  fictb 16101  finsschain 16102  nn0prpwlem 16110  nn0prpw 16111  qredeq 16112  2ndcctbss 16174  fnetr 16191  topbasfne 16195  fnessref 16199  neibastop1 16214  neibastop2lem2 16216  neibastop2lem3 16217  neibastop3 16220  topmtcl 16221  fnejoin1 16226  fnejoin2 16227  t0dist 16237  t1sep 16242  regsep 16246  nrmsep 16250  nrmsep2 16251  fmfnfmlem1 16292  flimfbas 16299  fclsfnflim 16312  fcluscomplem 16318  fzmul 16460  fdc 16475  seqpo 16477  incsequz 16478  heibor1lem 16539  ghomco 16581  zerdivemp1x 16594  pridlc 16704  ceqsex3OLD 16734  pm14.24 16869  sb5ALT 16967  truniALT 16984  onfrALTlem3 16988  ee223 17060  3orbi123VD 17208  sbc3orgVD 17209  exbirVD 17211  exbiriVD 17212  sbcim2gVD 17233  trsbcVD 17235  truniALTVD 17236  onfrALTlem3VD 17245  onfrALTlem2VD 17247  csbrngVD 17254  19.41rgVD 17260  a9e2eqVD 17265  a9e2ndeqVD 17267  2uasbanhVD 17269  sb5ALTVD 17270  vk15.4jVD 17271  pexmidALT 19643  cdleme18d 20016  tendovalco 20509  cdlemn11pre 20946  dihord2pre 20961
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
Copyright terms: Public domain