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

Theorem com12 27
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 28  syl6com 31  mpcom 32  syli 33  pm2.27 35  pm2.43b 47  syl9r 70  imim1OLD 74  com3r 79  pm2.86i 98  pm2.24 109  con3rr3 141  expt 161  jad 169  pm2.61dOLD 172  pm2.61 180  pm2.6OLD 182  biimpcdOLD 230  syl5ibcom 245  syl5ibrcom 249  biimprcdOLD 255  pm5.501 379  jaod 423  orel1 424  orel2OLD 426  pm2.62 454  pm2.621OLD 458  impcom 475  imp3a 476  expcom 480  exp3a 481  pm3.21 488  anim12iiOLD 626  imdistanri 765  pm2.64 831  pm2.75 892  ccased 995  dedlem0aOLD 1001  dedlem0b 1002  3impd 1241  3expd 1244  mp3an1i 1369  meredith 1385  simplbi2com 1484  a9wa9lem2 1592  a9wa9lem2OLD 1593  a9wa9lem6OLD 1598  hbimd 1690  19.21t 1693  equtrr 1710  sbequ2 1755  ax11b 1798  sb6rf 1840  sb56 1846  exmoeu 2008  moimv 2014  eupickbi 2032  2eu1 2046  exists2 2056  r19.12 2392  2gencl 2511  2genclOLD 2512  3gencl 2513  3genclOLD 2514  rcla4cv 2571  ceqex 2585  euind 2641  reuind 2652  sseq2 2825  uniiunlem 2879  disjne 3090  uneqdifeq 3125  difsn 3298  eqsn 3313  preq12b 3322  intab 3410  iinss2 3463  trint0 3581  dtru 3651  sspwb 3670  pocl 3757  pofun 3764  solin 3772  frss 3787  fr2nr 3791  efrirr 3794  tz7.7 3838  ordtri3 3848  ordtr2 3856  suc11 3914  onssneli 3920  eusv2OLD 3964  eusv2 3965  ralxfr 3986  iunpw 4005  fr3nr 4006  ordom 4096  peano5 4110  2optocl 4202  3optocl 4203  ssrel 4216  ssrelrel 4225  relop 4261  sotri3 4454  xp11 4482  relcnvtr 4546  fss 4697  fv3 4814  tz6.12-1 4817  tz6.12c 4821  tz6.12i 4822  fvco2 4859  fvopab2 4876  fornex 4924  funfvima 4985  fvclss 4989  f1fveq 5014  isotr 5039  isotrALT 5040  isomin 5041  oprabid 5071  poxp 5350  soxp 5351  iotaval 5368  smores 5402  smoel 5410  smogt 5417  smoiso2 5419  smoge 5420  tfrlem2 5422  tfrlem9 5430  tfr3 5437  tz7.48-2 5466  tz7.48-2OLD 5467  tz7.48-3 5469  tz7.49OLD 5470  tz7.49 5472  abianfp 5475  oecl 5524  oaordex 5544  oalimcl 5546  oaass 5547  oarec 5548  omordi 5549  omlimcl 5561  odi 5562  omeulem1 5565  oen0 5568  oewordri 5574  oeworde 5575  oaabs 5611  omsmolem 5615  2ecoptocl 5668  3ecoptocl 5669  eceqopreq 5677  th3qlem2 5679  dom3d 5774  xpdom2 5818  infensuc 5943  php 5949  onomeneq 5954  unxpdomlem2 5968  unxpdomlem3 5969  isinf 5978  domfi 5987  findcard 5995  findcard2 5996  unblem2 6007  unifi 6025  indexfi 6028  supub 6055  suplub 6056  supsnALT 6069  ordiso 6070  ordtypelem3 6073  ordtypelem4 6074  ordtypelem6 6076  ordtypelem7 6077  ordtype 6078  hartogs 6080  card2on 6083  card2inf 6084  elirrv 6090  inf3lem1 6108  inf3lem2 6109  inf3lem3 6110  inf3lem5 6112  noinfep 6138  noinfepOLD 6139  trcl 6140  tcel 6161  r1sdom 6172  rankr1c 6216  rankelbOLD 6219  rankval3b 6220  rankr1 6229  rankel 6235  rankxpsuc 6276  truniALT 6290  onfrALTlem3 6294  scottex 6311  carddomi2 6351  ondomcard 6359  pr2ne 6374  dif1card 6376  dif1cardOLD 6377  omsubsdomlem2 6404  elomsubsd 6409  infenomsub 6413  aceq3lem 6419  aceq8clem 6434  fodomnum 6442  cardaleph 6447  cflim2 6516  cfsmolem 6522  domtriomlem 6535  axdc3lem4 6545  axdc4lem 6547  kmlem4 6579  kmlem9 6584  kmlem12 6587  kmlem13 6588  numthlem 6594  zorn2lem3 6601  zorn2lem4 6602  zorn2lem5 6603  zorn2lem6 6604  zorn2lem7 6605  zornn0 6609  axdclem 6610  axdclem2 6611  ondomon 6646  alephval2 6653  cfpwsdom 6680  tsksdom 6710  tskssel2 6711  tsk2 6717  tskr1om 6719  grupr 6744  gruiun 6746  ingru 6761  grothomex 6775  axrepnd 6790  indpi 6881  nqereu 6904  genpnnp 6980  prlem934 7008  ltaddpr2 7010  reclem2pr 7023  mulgt0sr 7079  supsrlem 7085  mul0ori 7538  lemul1a 7677  squeeze0 7752  nnunb 7985  dfuzi 8100  fzind 8113  nn0ind-raph 8116  zindd 8117  uzwo3lem1 8119  eluzadd 8152  uzin 8155  suprzcl 8200  monoord 8382  icoshft 8446  fzen 8485  fzss1 8502  seqf2 8588  seqfveq2 8590  serf1o 8604  seq1rn2 8635  seqzrn2 8689  expcllem 8711  expeq0 8721  expgt0 8724  expgt1 8727  mulexp 8729  exprec 8730  exprecOLD 8731  bernneq 8798  bernneqOLD 8799  cjexp 8891  sqrmo 8928  absexp 9001  abssubne0 9016  cvg2i 9056  facdiv 9091  fseq1hash 9135  fsumrev 9203  2climnn 9282  2climnn0 9283  iserzmulc1 9318  caucvglem6 9344  caucvgi 9345  cvgratlem1 9434  cvgratlem2 9435  sin01bndlem2 9665  cos01bndlem2 9667  sin01gt0 9673  alzdvds 9801  dvdslegcd 9831  gcdneg 9840  mulgcdlem2 9867  exprmfctlem 9895  1arithlem22 9932  1arithlem30 9941  lmodlema 10287  tgcl 10474  tgss2 10487  subbas2 10495  distop 10499  ssnei2 10603  opnnei 10607  cnpnei 10656  cnpco 10659  cncnplem2 10665  meteq0 10697  neibl 10765  metequivlem 10773  caun0 10841  caubl 10865  xplmi 10872  lmcau 10895  gxnn0add 10993  gxnn0mul 10996  isga 11048  ssga 11053  gagrpid 11056  gaass 11057  gapmlem 11059  vacnlem3 11265  vacnlem6 11268  ipassi 11433  ubthlem2 11464  pslem 11557  spwmo 11565  efifolem5 11642  hmeobc 11758  cnvhmpha 11759  fbfinnfr 11775  isfildlem 11785  snfil 11793  fbunfip 11796  fgfild 11804  limfilss 11815  elfm2 11830  flimopn 11837  cncomp 11847  usinuniop 11857  ismgm 11885  isexid2 11890  grpomnd 11911  rnplrnml0 11920  on1el4 11931  isch3 12261  projlem28 12360  projlem29 12361  pjthlem14 12379  shintcli 12441  shmodsi 12508  spansni 12626  spansncvi 12743  pjjsi 12791  hoaddsub 12890  eigorthi 12911  homco2 13048  cnlnadjlem5 13140  pjss2coi 13234  pjnormssi 13238  pj3cor1i 13280  strb 13329  dmdmd 13371  mdsl0 13381  csmdsymi 13405  chrelat2i 13436  cvati 13437  mdsymlem3 13476  mdsymlem6 13479  sumdmdlem2 13490  dmdbr5ati 13493  nqereuNEW 13532  fsumlem 13588  isummulc1NEW 13609  isumdivcNEW 13611  dfuziNEW 13623  prmpwdvds 13717  fseq1cl 13968  3ccased 14006  dedekind 14019  rprimelpwr 14063  dfres3 14109  dfon2lem3 14137  omssadd 14150  rdgprc 14159  trpredmintr 14241  trpredrec 14248  wfr3g 14262  wfrlem12 14274  frr3g 14287  frrlem11 14300  sltval2 14316  axfelem13 14365  brtxp2 14435  elfuns 14461  axcontlem4 14597  cgrextend 14633  btwndiff 14652  btwnconn1lem12 14723  brsegle 14733  broutsideof2 14747  funray 14765  meran1 14916  waj-ax 14919  arg-ax 14921  wl-pm2.86i 14964  coprsexg 15005  evpexun 15031  uninqs 15049  cpref 15085  inttr 15090  isunscov 15092  restidsing 15096  twsymr 15099  prj1b 15100  prj3 15101  set2elt 15113  fixpc 15123  surjsec 15153  injrec2 15154  surjsec2 15155  eloprvdm2 15164  domintrefc 15165  mapmapmap 15192  injsurinj 15193  prmapcp2 15204  npincppr 15208  repfuntw 15209  repcpwti 15210  cbcpcp 15211  prjmapcp 15214  cbicplem 15215  unprj 15218  prl 15219  prl2 15221  prjmapcp2 15222  dstr 15223  nZdef 15232  jidd 15247  midd 15248  preotr2 15283  int2pre 15285  ubpar 15310  inposet 15327  tolat 15338  pospos 15342  toplat 15345  latdir 15350  fprod1ib 15393  ridlideq 15398  rzrlzreq 15399  clfsebs 15410  resgcom 15415  symgfo 15433  curgrpact 15438  grpodivone 15439  grpodivfo 15440  cmprltr 15480  rltrran 15484  zerdivemp1 15506  zintdom 15508  muldisc 15552  svli2 15554  svs2 15557  truni1 15577  truni2 15578  truni3 15579  inttop2 15588  neffopo 15593  npmp 15596  mapdiscnlem 15603  mapdiscn 15604  mapudiscn 15605  nsn 15607  cnvhmphb 15613  hmphre 15617  hmeogrp 15625  homcard 15626  top2ind 15630  top2usne 15631  homindlem3 15633  intopcoaconlem3b 15634  intopcoaconc 15637  qusp 15638  intcont 15642  prtoptop 15648  prcnt 15650  efilcp 15651  fisub 15653  fbaslim2 15660  limfilnei 15667  conttnf 15668  iscnp3 15670  cnpfillim4 15671  cmptdst 15675  limhun 15677  exopcopn 15679  prdnei 15680  limptlimpr2lem1 15681  limptlimpr2lem2 15682  flimfnei2 15684  islimrs 15687  islimrs3 15688  islimrs4 15689  bwt2 15706  grpohmlem1 15731  grpohmlem2 15732  grpohlem3 15733  grpohmlem4 15734  grpohlem5 15735  grpohm 15736  cntrsetlem 15748  iintlem1 15757  iint 15759  cnvtr 15763  mlteqer 15764  xrletr2 15765  lteqtpos 15771  lvsovso 15787  lvsovso3 15789  supnuf 15790  addcomv 15809  addidv2 15811  cnegvex2 15813  addcanri 15817  addcanrg 15818  negveud 15819  issubcv 15820  cmppfd 15873  domcmpd 15874  codcmpd 15875  cmpasso 15901  cmpida 15902  cmpidb 15903  dualalg 15912  dualded 15913  dualcat2 15914  cmpassoh 15931  homgrf 15932  imonclem 15943  cmpmon 15945  iepiclem 15953  isepic 15954  idfisf 15970  tartrel 16014  tartord 16015  cptarc 16017  sexptrt 16018  tarsuc2 16020  bpmp 16026  btmp 16027  intartar 16030  tartarmap 16040  vtarsuelt 16047  partarelt1 16048  inttaror 16052  inttarcar 16053  cartarlim 16057  fnctartar 16059  fnctartar2 16060  prismorcset2 16071  morexcmp 16120  cmpmor 16128  setiscat 16132  lemindclsbu 16183  indcls2 16184  indclsbusuc 16189  clscnc 16202  pgapspf2 16245  elicc3 16278  dfnn3 16281  fictb 16286  finsschain 16287  nn0prpwlem 16296  nn0prpw 16297  qredeq 16298  compfipin0 16333  dfcon2 16339  reconn 16348  iccconn 16350  2ndcctbss 16375  fnetr 16392  topbasfne 16396  fnessref 16400  neibastop1 16415  neibastop2lem2 16417  neibastop2lem3 16418  neibastop3 16421  topmtcl 16422  fnejoin1 16427  fnejoin2 16428  t0dist 16438  t1sep 16443  regsep 16447  nrmsep 16451  nrmsep2 16452  fmfnfmlem1 16493  flimfbas 16500  fclsfnflim 16513  fcluscomplem 16519  oprabvalg 16603  eropreu 16628  fzmul 16679  sdclem1 16696  sdclem2 16697  sdc 16698  fdc 16699  seqpo 16701  incsequz 16702  iccss2 16742  heibor1lem 16842  ghomco 16897  pcohtpy 16940  zerdivemp1x 16964  pridlc 17074  ceqsex3OLD 17104  pm14.24 17241  sb5ALT 17316  ee223 17372  3orbi123VD 17520  sbc3orgVD 17521  exbirVD 17523  exbiriVD 17524  sbcim2gVD 17545  trsbcVD 17547  truniALTVD 17548  onfrALTlem3VD 17557  onfrALTlem2VD 17559  csbrngVD 17566  19.41rgVD 17572  a9e2eqVD 17577  a9e2ndeqVD 17579  sb5ALTVD 17580  vk15.4jVD 17581  pexmidALT 19960  cdleme18d 20325  tendovalco 20818  cdlemn11pre 21258  dihord2pre 21273
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-mp 7
Copyright terms: Public domain