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 1576  19.21t 1579  equtrr 1596  sbequ2 1641  ax11b 1684  sb6rf 1726  sb56 1732  exmoeu 1894  moimv 1900  eupickbi 1918  2eu1 1932  exists2 1942  r19.12 2273  2gencl 2394  3gencl 2395  rcla4cv 2449  ceqex 2464  euind 2520  reuind 2531  sseq2 2706  uniiunlem 2758  disjne 2970  uneqdifeq 3005  difsn 3184  eqsn 3199  preq12b 3208  intab 3297  iinss2 3350  trint0 3464  dtru 3533  sspwb 3552  pocl 3639  pofun 3648  solin 3656  frss 3672  fr2nr 3676  efrirr 3679  tz7.7 3723  ordtri3 3733  ordtr2 3741  suc11 3798  onssneli 3804  eusv2 3848  ralxfrALT 3872  iunpw 3893  fr3nr 3894  ordom 3984  peano5 3998  2optocl 4094  3optocl 4095  ssrel 4108  ssrelrel 4117  relop 4152  sotri3 4347  xp11 4377  relcnvtr 4439  fss 4582  fv3 4700  tz6.12-1 4703  tz6.12c 4707  tz6.12i 4708  fvco2 4746  fvopab2 4763  fornex 4813  funfvima 4868  fvclss 4872  f1fveq 4898  isotr 4923  isotrALT 4924  isomin 4925  oprabid 4956  ovg 5020  poxp 5266  soxp 5267  iotaval 5284  smores 5318  smoel 5326  smogt 5333  smoiso2 5335  smoge 5336  tfrlem2 5338  tfrlem9 5346  tfr3 5353  tz7.48-2 5382  tz7.48-3 5384  tz7.49 5385  abianfp 5388  oecl 5437  oaordex 5457  oalimcl 5459  oaass 5460  oarec 5461  omordi 5462  omlimcl 5474  odi 5475  omeulem1 5478  oen0 5481  oewordri 5487  oeworde 5488  oaabs 5524  omsmolem 5528  2ecoptocl 5595  3ecoptocl 5596  eceqoveq 5610  th3qlem2 5612  dom3d 5716  xpdom2 5760  infensuc 5882  php 5888  onomeneq 5893  unxpdomlem2 5907  unxpdomlem3 5908  isinf 5917  domfi 5926  findcard 5933  findcard2 5934  unblem2 5945  unifi 5963  indexfi 5966  supub 6007  suplub 6008  supsnALT 6021  ordiso 6022  ordtypelem3 6025  ordtypelem4 6026  ordtypelem6 6028  ordtypelem7 6029  ordtype 6030  hartogs 6032  card2on 6035  card2inf 6036  elirrv 6042  inf3lem1 6060  inf3lem2 6061  inf3lem3 6062  inf3lem5 6064  noinfep 6088  noinfepOLD 6089  trcl 6090  tcel 6110  r1sdom 6121  rankr1c 6161  rankval3b 6164  rankr1 6172  rankel 6178  rankxpsuc 6218  scottex 6221  carddomi2 6261  ondomcard 6269  pr2ne 6284  dif1card 6286  omsubsdomlem2 6313  elomsubsd 6318  infenomsub 6322  aceq3lem 6328  aceq8clem 6343  fodomnum 6351  cardaleph 6356  cflim2 6425  cfsmolem 6431  domtriomlem 6444  axdc3lem4 6454  axdc4lem 6456  kmlem4 6488  kmlem9 6493  kmlem12 6496  kmlem13 6497  numthlem 6503  zorn2lem3 6510  zorn2lem4 6511  zorn2lem5 6512  zorn2lem6 6513  zorn2lem7 6514  zornn0 6518  axdclem 6519  axdclem2 6520  ondomon 6555  alephval2 6562  cfpwsdom 6589  axrepnd 6599  tsksdom 6653  tskssel2 6654  tsk2 6660  tskr1om 6662  grupr 6687  gruiun 6689  ingru 6704  grothomex 6718  indpi 6791  nqereu 6814  genpnnp 6890  prlem934 6918  ltaddpr2 6920  reclem2pr 6933  mulgt0sr 6989  supsrlem 6995  mul0ori 7457  lemul1a 7593  squeeze0 7657  peano5nni 7706  nnunb 7870  fzind 8000  nn0ind-raph 8003  zindd 8004  eluzadd 8063  uzin 8066  suprzcl 8113  ico0 8317  ioc0 8318  iccss2 8333  icoshft 8364  fzen 8416  fzss1 8433  expcllem 8630  expeq0 8644  mulexp 8653  expword2i 8670  bernneq 8732  facdiv 8763  hashmap 8822  cjexp 8911  sqrmo 8967  absexp 9041  abssubne0 9056  caurcvg 9173  sin01gt0 9441  alzdvds 9547  dvdslegcd 9581  gcdneg 9590  rprimelpwr 9619  exprmfctlem 9666  prmpwdvds 9769  prmreclem4 9784  pslem 10062  spwmo 10073  gxnn0add 10520  gxnn0mul 10523  ismgm 10572  isexid2 10577  grpomnd 10598  isga 10628  ssga 10633  gagrpid 10636  gaass 10637  gapmlem 10639  rngodm1dm2 10692  rngosn4 10703  fiinopn 10733  tgcl 10777  tgss2 10791  distop 10802  ssnei2 10892  opnnei 10896  cnpnei 10949  cnpco 10952  cncnplem2 10958  cncmp 10985  cmpfi 10997  usinuniop 11002  dfcon2 11003  cnmptcom 11042  fbfinnfr 11070  isfildlem 11080  snfil 11088  fbunfip 11091  fgfild 11099  limfilss 11111  elfm2 11126  flimopn 11133  meteq0 11158  neibl 11229  metequivlem 11237  reconn 11302  iccconn 11304  pi1gplem 11394  caubl 11452  ipassi 11791  ubthlem2 11822  minveclem5 11832  volsuplem 11991  cxpmul2 12508  isch3 12889  shintcli 12977  shmodsi 13037  spansncvi 13318  pjjsi 13366  hoaddsub 13465  eigorthi 13486  homco2 13625  cnlnadjlem5 13719  pjss2coi 13812  pjnormssi 13816  pj3cor1i 13857  strb 13906  dmdmd 13948  mdsl0 13958  csmdsymi 13982  chrelat2i 14013  cvati 14014  mdsymlem3 14053  mdsymlem6 14056  sumdmdlem2 14067  dmdbr5ati 14070  3ccased 14239  dedekind 14245  dfres3 14287  dfon2lem3 14317  omssadd 14330  rdgprc 14339  trpredmintr 14426  trpredrec 14433  wfr3g 14447  wfrlem12 14459  frr3g 14472  frrlem11 14485  sltval2 14501  axfelem13 14550  elfuns 14652  axcontlem4 14790  cgrextend 14826  btwndiff 14845  btwnconn1lem12 14916  brsegle 14926  broutsideof2 14940  funray 14958  meran1 15120  waj-ax 15123  arg-ax 15125  wl-pm2.86i 15168  copsexgb 15208  evpexun 15236  cpref 15290  inttr 15295  isunscov 15297  restidsing 15301  twsymr 15303  prj1b 15304  prj3 15305  set2elt 15317  fixpc 15326  surjsec 15356  injrec2 15357  surjsec2 15358  elovdm2 15366  domintrefc 15367  elico3 15384  elioc3 15385  mapmapmap 15394  injsurinj 15395  repfuntw 15407  repcpwti 15408  cbcpcp 15409  unprj 15414  prl 15415  prl2 15417  prjmapcp2 15418  dstr 15419  nZdef 15428  jidd 15440  midd 15441  preotr2 15475  int2pre 15477  ubpar 15503  inposet 15520  tolat 15531  pospos 15535  toplat 15538  latdir 15543  ridlideq 15585  rzrlzreq 15586  resgcom 15602  symgfo 15620  curgrpact 15625  grpodivone 15626  grpodivfo 15627  rltrran 15668  zerdivemp1 15690  zintdom 15692  muldisc 15734  svli2 15737  svs2 15740  truni1 15758  truni2 15759  truni3 15760  inttop2 15769  npmp 15775  mapdiscnlem 15782  mapdiscn 15783  mapudiscn 15784  nsn 15786  top2ind 15811  top2usne 15812  homindlem3 15814  intopcoaconlem3b 15815  intopcoaconc 15818  qusp 15819  intcont 15820  prtoptop 15826  prcnt 15828  efilcp 15829  fisub 15831  fbaslim2 15838  limfilnei 15845  conttnf 15846  iscnp3 15848  cnpfillim4 15849  cmptdst 15853  limhun 15855  exopcopn 15857  prdnei 15858  limptlimpr2lem1 15859  limptlimpr2lem2 15860  flimfnei2 15862  islimrs 15865  islimrs3 15866  islimrs4 15867  bwt2 15882  grpohmlem1 15907  grpohmlem2 15908  grpohlem3 15909  grpohmlem4 15910  grpohlem5 15911  grpohm 15912  iintlem1 15932  iint 15934  cnvtr 15938  mlteqer 15939  xrletr2 15940  lteqtpos 15946  lvsovso 15962  lvsovso3 15964  supnuf 15965  claddrvr 15984  sigadd 15985  addcomv 15991  cnegvex2 15996  addcanri 16002  addcanrg 16003  negveud 16004  negveudr 16005  issubcv 16006  subaddv 16007  subclrvd 16010  distsava 16025  intvconlem1 16041  consuba 16044  hdrmp 16047  cmppfd 16089  domcmpd 16090  codcmpd 16091  cmpasso 16117  cmpida 16118  cmpidb 16119  dualalg 16128  dualded 16129  dualcat2 16130  cmpassoh 16147  homgrf 16148  imonclem 16159  cmpmon 16161  iepiclem 16169  isepic 16170  idfisf 16186  propsrc 16211  tartrel 16231  tartord 16232  cptarc 16234  sexptrt 16235  tarsuc2 16237  bpmp 16243  btmp 16244  intartar 16247  tartarmap 16257  vtarsuelt 16264  partarelt1 16265  inttaror 16269  inttarcar 16270  cartarlim 16274  fnctartar 16276  fnctartar2 16277  prismorcset2 16288  morexcmp 16337  cmpmor 16345  setiscat 16349  lemindclsbu 16400  indcls2 16401  clscnc 16415  pgapspf2 16458  elicc3 16491  fictb 16496  finsschain 16497  nn0prpwlem 16505  nn0prpw 16506  qredeq 16507  2ndcctbss 16565  fnetr 16582  topbasfne 16586  fnessref 16590  neibastop1 16605  neibastop2lem2 16607  neibastop2lem3 16608  neibastop3 16611  topmtcl 16612  fnejoin1 16617  fnejoin2 16618  t0dist 16628  t1sep 16633  regsep 16637  nrmsep 16641  nrmsep2 16642  fmfnfmlem1 16683  flimfbas 16690  fclsfnflim 16703  fcluscomplem 16709  fzmul 16851  fdc 16866  seqpo 16868  incsequz 16869  heibor1lem 16930  ghomco 16972  zerdivemp1x 16985  pridlc 17095  ceqsex3OLD 17125  pm14.24 17260  sb5ALT 17358  truniALT 17375  onfrALTlem3 17379  ee223 17451  3orbi123VD 17599  sbc3orgVD 17600  exbirVD 17602  exbiriVD 17603  sbcim2gVD 17624  trsbcVD 17626  truniALTVD 17627  onfrALTlem3VD 17636  onfrALTlem2VD 17638  csbrngVD 17645  19.41rgVD 17651  a9e2eqVD 17656  a9e2ndeqVD 17658  2uasbanhVD 17660  sb5ALTVD 17661  vk15.4jVD 17662  pexmidALT 20034  cdleme18d 20407  tendovalco 20900  cdlemn11pre 21338  dihord2pre 21353
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
Copyright terms: Public domain