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

Theorem com12 26
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 25 1 |- (ps -> (ph -> ch))
Colors of variables: wff set class
Syntax hints:   -> wi 4
This theorem is referenced by:  syl5 27  syl6com 30  mpcom 31  syli 32  pm2.27 34  pm2.43b 45  syl9r 66  com3r 72  pm2.86i 91  pm2.24 99  con3rr3 125  expt 145  jad 151  pm2.61dOLD 154  pm2.61 162  pm2.6OLD 164  biimpcdOLD 211  syl5ibcom 224  syl5ibrcom 226  biimprcdOLD 230  pm5.501 345  jaod 388  orel1 389  pm2.62 418  pm2.621OLD 421  impcom 438  imp3a 439  expcom 443  exp3a 444  pm3.21 451  imdistanri 690  pm2.64 753  pm2.75 815  ccased 915  dedlem0b 921  3impd 1162  3expd 1165  mp3an1i 1266  meredith 1282  simplbi2com 1362  a9wa9lem2 1468  a9wa9lem2OLD 1469  a9wa9lem6OLD 1474  hbimd 1568  19.21t 1571  equtrr 1588  sbequ2 1633  ax11b 1676  sb6rf 1718  sb56 1724  exmoeu 1886  moimv 1892  eupickbi 1910  2eu1 1924  exists2 1934  r19.12 2265  2gencl 2386  3gencl 2387  rcla4cv 2441  ceqex 2456  euind 2512  reuind 2523  sseq2 2700  uniiunlem 2752  disjne 2964  uneqdifeq 2999  difsn 3178  eqsn 3193  preq12b 3202  intab 3291  iinss2 3344  trint0 3458  dtru 3527  sspwb 3546  pocl 3633  pofun 3642  solin 3650  frss 3666  fr2nr 3670  efrirr 3673  tz7.7 3717  ordtri3 3727  ordtr2 3735  suc11 3792  onssneli 3798  eusv2 3842  ralxfrALT 3868  iunpw 3889  fr3nr 3890  ordom 3980  peano5 3994  2optocl 4090  3optocl 4091  ssrel 4104  ssrelrel 4113  relop 4148  sotri3 4343  xp11 4373  relcnvtr 4435  fss 4578  fv3 4696  tz6.12-1 4699  tz6.12c 4703  tz6.12i 4704  fvco2 4742  fvopab2 4759  fornex 4809  funfvima 4864  fvclss 4868  f1fveq 4894  isotr 4919  isotrALT 4920  isomin 4921  oprabid 4952  ovg 5016  poxp 5263  soxp 5264  iotaval 5281  smores 5315  smoel 5323  smogt 5330  smoiso2 5332  smoge 5333  tfrlem2 5335  tfrlem9 5343  tfr3 5350  tz7.48-2 5379  tz7.48-3 5381  tz7.49 5382  abianfp 5385  oecl 5434  oaordex 5454  oalimcl 5456  oaass 5457  oarec 5458  omordi 5459  omlimcl 5471  odi 5472  omeulem1 5475  oen0 5478  oewordri 5484  oeworde 5485  oaabs 5521  omsmolem 5525  2ecoptocl 5592  3ecoptocl 5593  eceqoveq 5607  th3qlem2 5609  dom3d 5713  xpdom2 5757  infensuc 5879  php 5885  onomeneq 5890  unxpdomlem2 5904  unxpdomlem3 5905  isinf 5914  domfi 5923  findcard 5930  findcard2 5931  unblem2 5942  unifi 5960  indexfi 5963  supub 6005  suplub 6006  supsnALT 6020  ordiso 6021  ordtypelem3 6024  ordtypelem4 6025  ordtypelem6 6027  ordtypelem7 6028  ordtype 6029  hartogs 6031  card2on 6034  card2inf 6035  elirrv 6041  inf3lem1 6059  inf3lem2 6060  inf3lem3 6061  inf3lem5 6063  noinfep 6087  noinfepOLD 6088  trcl 6089  tcel 6109  r1sdom 6120  rankr1c 6160  rankval3b 6163  rankr1 6171  rankel 6177  rankxpsuc 6217  scottex 6220  carddomi2 6260  ondomcard 6268  pr2ne 6283  dif1card 6285  omsubsdomlem2 6312  elomsubsd 6317  infenomsub 6321  aceq3lem 6327  aceq8clem 6342  fodomnum 6350  cardaleph 6355  cflim2 6424  cfsmolem 6430  domtriomlem 6443  axdc3lem4 6453  axdc4lem 6455  kmlem4 6487  kmlem9 6492  kmlem12 6495  kmlem13 6496  numthlem 6502  zorn2lem3 6509  zorn2lem4 6510  zorn2lem5 6511  zorn2lem6 6512  zorn2lem7 6513  zornn0 6517  axdclem 6518  axdclem2 6519  ondomon 6554  alephval2 6561  cfpwsdom 6588  axrepnd 6598  tsksdom 6652  tskssel2 6653  tsk2 6659  tskr1om 6661  grupr 6686  gruiun 6688  ingru 6703  grothomex 6717  indpi 6790  nqereu 6813  genpnnp 6889  prlem934 6917  ltaddpr2 6919  reclem2pr 6932  mulgt0sr 6988  supsrlem 6994  mul0ori 7457  lemul1a 7593  squeeze0 7657  peano5nni 7706  nnunb 7870  fzind 8000  nn0ind-raph 8003  zindd 8004  eluzadd 8063  uzin 8066  suprzcl 8113  ico0 8319  ioc0 8320  iccss2 8335  icoshft 8366  fzen 8418  fzss1 8435  expcllem 8632  expeq0 8647  mulexp 8656  expword2i 8673  bernneq 8735  facdiv 8766  hashmap 8826  cjexp 8911  sqrmo 8968  absexp 9042  abssubne0 9058  sin01gt0 9457  alzdvds 9563  dvdslegcd 9597  gcdneg 9606  rprimelpwr 9635  exprmfctlem 9682  prmpwdvds 9791  prmreclem4 9806  pslem 10084  spwmo 10095  gxnn0add 10582  gxnn0mul 10585  ismgm 10634  isexid2 10639  grpomnd 10660  isga 10690  ssga 10695  gagrpid 10698  gaass 10699  gapmlem 10701  rngodm1dm2 10754  rngosn4 10765  fiinopn 10795  tgcl 10839  tgss2 10853  distop 10864  ssnei2 10954  opnnei 10958  cnpnei 11011  cnpco 11014  cncnplem2 11020  cncmp 11047  cmpfi 11059  usinuniop 11064  dfcon2 11065  cnmptcom 11106  fbfinnfr 11134  isfildlem 11144  snfil 11152  fbunfip 11155  fgfild 11163  limfilss 11175  elfm2 11190  flimopn 11197  meteq0 11222  neibl 11293  metequivlem 11301  reconn 11367  iccconn 11369  pi1gplem 11459  caubl 11517  ipassi 11856  ubthlem2 11887  minveclem5 11897  volsuplem 12061  cxpmul2 12672  qabvexp 12743  isch3 13086  shintcli 13174  shmodsi 13234  spansncvi 13515  pjjsi 13563  hoaddsub 13662  eigorthi 13683  homco2 13822  cnlnadjlem5 13916  pjss2coi 14009  pjnormssi 14013  pj3cor1i 14054  strb 14103  dmdmd 14145  mdsl0 14155  csmdsymi 14179  chrelat2i 14210  cvati 14211  mdsymlem3 14250  mdsymlem6 14253  sumdmdlem2 14264  dmdbr5ati 14267  3ccased 14436  dedekind 14442  dfres3 14484  dfon2lem3 14514  omssadd 14527  rdgprc 14536  trpredmintr 14623  trpredrec 14630  wfr3g 14644  wfrlem12 14656  frr3g 14669  frrlem11 14682  sltval2 14698  axfelem13 14747  elfuns 14849  axcontlem4 14987  cgrextend 15023  btwndiff 15042  btwnconn1lem12 15113  brsegle 15123  broutsideof2 15137  funray 15155  meran1 15317  waj-ax 15320  arg-ax 15322  wl-pm2.86i 15365  copsexgb 15405  evpexun 15433  cpref 15487  inttr 15492  isunscov 15494  restidsing 15498  twsymr 15500  prj1b 15501  prj3 15502  set2elt 15514  fixpc 15523  surjsec 15553  injrec2 15554  surjsec2 15555  elovdm2 15563  domintrefc 15564  elico3 15581  elioc3 15582  mapmapmap 15591  injsurinj 15592  repfuntw 15604  repcpwti 15605  cbcpcp 15606  unprj 15611  prl 15612  prl2 15614  prjmapcp2 15615  dstr 15616  nZdef 15625  jidd 15637  midd 15638  preotr2 15672  int2pre 15674  ubpar 15700  inposet 15717  tolat 15728  pospos 15732  toplat 15735  latdir 15740  ridlideq 15782  rzrlzreq 15783  resgcom 15799  symgfo 15817  curgrpact 15822  grpodivone 15823  grpodivfo 15824  rltrran 15865  zerdivemp1 15887  zintdom 15889  muldisc 15931  svli2 15934  svs2 15937  truni1 15955  truni2 15956  truni3 15957  inttop2 15966  npmp 15972  mapdiscnlem 15979  mapdiscn 15980  mapudiscn 15981  nsn 15983  top2ind 16008  top2usne 16009  homindlem3 16011  intopcoaconlem3b 16012  intopcoaconc 16015  qusp 16016  intcont 16017  prtoptop 16023  prcnt 16025  efilcp 16026  fisub 16028  fbaslim2 16035  limfilnei 16042  conttnf 16043  iscnp3 16045  cnpfillim4 16046  cmptdst 16050  limhun 16052  exopcopn 16054  prdnei 16055  limptlimpr2lem1 16056  limptlimpr2lem2 16057  flimfnei2 16059  islimrs 16062  islimrs3 16063  islimrs4 16064  bwt2 16079  grpohmlem1 16104  grpohmlem2 16105  grpohmlem3 16106  grpohmlem4 16107  grpohmlem5 16108  grpohm 16109  iintlem1 16129  iint 16131  cnvtr 16135  mlteqer 16136  xrletr2 16137  lteqtpos 16143  lvsovso 16159  lvsovso3 16161  supnuf 16162  claddrvr 16181  sigadd 16182  addcomv 16188  cnegvex2 16193  addcanri 16199  addcanrg 16200  negveud 16201  negveudr 16202  issubcv 16203  subaddv 16204  subclrvd 16207  distsava 16222  intvconlem1 16238  consuba 16241  hdrmp 16244  cmppfd 16286  domcmpd 16287  codcmpd 16288  cmpasso 16314  cmpida 16315  cmpidb 16316  dualalg 16325  dualded 16326  dualcat2 16327  cmpassoh 16344  homgrf 16345  imonclem 16356  cmpmon 16358  iepiclem 16366  isepic 16367  idfisf 16383  propsrc 16408  tartrel 16428  tartord 16429  cptarc 16431  sexptrt 16432  tarsuc2 16434  bpmp 16440  btmp 16441  intartar 16444  tartarmap 16454  vtarsuelt 16461  partarelt1 16462  inttaror 16466  inttarcar 16467  cartarlim 16471  fnctartar 16473  fnctartar2 16474  prismorcset2 16485  morexcmp 16534  cmpmor 16542  setiscat 16546  lemindclsbu 16597  indcls2 16598  clscnc 16612  pgapspf2 16655  elicc3 16688  fictb 16693  finsschain 16694  nn0prpwlem 16701  nn0prpw 16702  qredeq 16703  2ndcctbss 16761  fnetr 16778  topbasfne 16782  fnessref 16786  neibastop1 16801  neibastop2lem2 16803  neibastop2lem3 16804  neibastop3 16807  topmtcl 16808  fnejoin1 16813  fnejoin2 16814  t0dist 16824  t1sep 16829  regsep 16833  nrmsep 16837  nrmsep2 16838  fmfnfmlem1 16879  flimfbas 16886  fclsfnflim 16899  fcluscomplem 16905  fzmul 17046  fdc 17061  seqpo 17063  incsequz 17064  heibor1lem 17125  ghomco 17167  zerdivemp1x 17180  pridlc 17290  ceqsex3OLD 17320  pm14.24 17455  sb5ALT 17553  truniALT 17570  onfrALTlem3 17574  ee223 17646  3orbi123VD 17794  sbc3orgVD 17795  exbirVD 17797  exbiriVD 17798  sbcim2gVD 17819  trsbcVD 17821  truniALTVD 17822  onfrALTlem3VD 17831  onfrALTlem2VD 17833  csbrngVD 17840  19.41rgVD 17846  a9e2eqVD 17851  a9e2ndeqVD 17853  2uasbanhVD 17855  sb5ALTVD 17856  vk15.4jVD 17857  pexmidALT 20229  cdleme18d 20604  tendovalco 21098  cdlemn11pre 21539  dihord2pre 21554
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
Copyright terms: Public domain