MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  com12 Unicode version

Theorem com12 29
Description: Inference that swaps (commutes) antecedents in an implication. (Contributed by NM, 5-Aug-1993.) (Proof 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 21 . 2  |-  ( ps 
->  ps )
2 com12.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
31, 2syl5com 28 1  |-  ( ps 
->  ( ph  ->  ch ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6
This theorem is referenced by:  syl5  30  syl6com  33  mpcom  34  syli  35  pm2.27  37  pm2.43b  48  syl9r  69  com3r  75  pm2.86i  94  pm2.24  103  con3rr3  130  expt  150  jad  156  pm2.61  165  syl5ibcom  213  syl5ibrcom  215  pm5.501  332  jaod  371  orel1  373  pm2.62  400  impcom  421  imp3a  422  expcom  426  exp3a  427  pm3.21  437  imdistanri  675  pm2.64  767  pm2.75  825  ccased  918  dedlem0b  924  3impd  1170  3expd  1173  mp3an1i  1275  simplbi2com  1370  meredith  1400  ax12olem21  1655  ax12olem23  1657  ax10lem16  1665  ax10lem26  1675  ax10  1677  hbimd  1809  equtrr  1827  sbequ2  1890  ax11b  1942  sb6rf  1985  sb56  1991  mo  2135  exmoeu  2155  moimv  2161  eupickbi  2179  2mo  2191  2eu1  2193  exists2  2203  r19.12  2616  2gencl  2753  3gencl  2754  rcla4cv  2816  ceqex  2833  mob  2882  euind  2887  reuind  2901  sseq2  3118  reupick2  3358  uneqdifeq  3445  difsn  3654  eqsn  3672  preq12b  3685  iinss2  3849  disjxiun  3914  trint0  4024  dtru  4092  sspwb  4114  copsexg  4142  pocl  4211  pofun  4220  solin  4227  frss  4250  tz7.7  4308  ordtri3  4318  ordtr2  4326  suc11  4384  onssneli  4390  reusv1  4422  reusv2lem1  4423  alxfr  4435  ralxfrALT  4441  iunpw  4458  ordom  4553  limom  4559  peano5  4567  2optocl  4669  3optocl  4670  ssrel  4680  ssrelrel  4691  relop  4738  asymref2  4964  xpidtr  4969  trin2  4970  sotri3  4977  poltletr  4982  xp11  5015  relcnvtr  5095  funmo  5126  fss  5251  fv3  5390  tz6.12-1  5393  tz6.12c  5397  tz6.12i  5398  mpteqb  5463  fornex  5599  funfvima  5602  fvclss  5609  f1fveq  5635  isoselem  5687  oprabid  5731  ovg  5835  poxp  6076  soxp  6077  tposfn2  6105  sorpsscmpl  6137  iotaval  6151  onnseq  6244  smoel  6260  smogt  6267  smoiso2  6269  tfrlem2  6275  tfr3  6298  tz7.48-2  6337  tz7.48-3  6339  tz7.49  6340  abianfp  6354  oecl  6419  oaordex  6439  oalimcl  6441  oaass  6442  omordi  6447  omlimcl  6459  odi  6460  omeulem1  6463  oen0  6467  oewordri  6473  nnawordi  6502  nnaass  6503  nnmordi  6512  omabs  6528  omsmolem  6534  iiner  6614  2ecoptocl  6632  3ecoptocl  6633  th3qlem2  6648  undifixp  6735  xpdom2  6839  xpf1o  6905  infensuc  6921  php  6927  onomeneq  6932  isinf  6958  findcard2  6980  unblem2  6992  finsschain  7043  marypha1  7068  hartogs  7140  card2on  7149  card2inf  7150  xpwdomg  7180  elirrv  7192  inf3lem1  7210  inf3lem2  7211  inf3lem3  7212  inf3lem5  7214  noinfep  7241  noinfepOLD  7242  trcl  7291  en3lp  7299  tcel  7311  r1sdom  7327  rankonidlem  7381  scottex  7436  pr2ne  7516  dif1card  7519  fodomnum  7565  cardaleph  7597  kmlem4  7660  kmlem9  7665  kmlem12  7668  kmlem13  7669  cflim2  7770  cfsmolem  7777  infpssrlem3  7812  isfin7-2  7903  fin1a2lem6  7912  fin1a2lem10  7916  fin1a2lem12  7918  domtriomlem  7949  axdc3lem4  7960  axdc4lem  7962  zorn2lem3  8006  zorn2lem4  8007  zorn2lem5  8008  zorn2lem6  8009  zorn2lem7  8010  zornn0g  8013  axdclem  8027  axdclem2  8028  ondomon  8064  alephval2  8071  cfpwsdom  8083  wunr1om  8218  wuncval2  8246  tskr1om  8266  grupr  8296  gruiun  8298  ingru  8314  grothomex  8328  indpi  8408  nqereu  8430  genpnnp  8506  prlem934  8534  ltaddpr2  8536  reclem2pr  8549  mulgt0sr  8604  supsrlem  8610  lemul1a  9458  squeeze0  9507  peano5nni  9597  nnunb  9807  fzind  9955  nn0ind-raph  9958  zindd  9959  eluzadd  10102  uzin  10106  xmulasslem  10450  icoshft  10603  fzen  10654  expcllem  10957  expeq0  10975  mulexp  10984  leexp2r  11002  bernneq  11069  facdiv  11142  hashmap  11228  cjexp  11476  absexp  11628  iseraltlem2  11994  sin01gt0  12306  alzdvds  12414  dvdslegcd  12531  gcdneg  12541  rplpwr  12571  qredeq  12621  prmpwdvds  12787  prmreclem4  12802  ramcl  12912  imasleval  13279  mreiincl  13332  drsdirfi  13878  spwmo  14132  efgi2  14831  fiinopn  16441  tgcl  16501  distop  16527  isclo2  16619  iscldtop  16626  ssnei2  16647  opnnei  16651  pnfnei  16744  mnfnei  16745  tgcnp  16777  cnpnei  16787  2ndcctbss  16975  1stcelcls  16981  txcnpi  17096  cnmptcom  17166  fbfinnfr  17330  isfildlem  17346  snfil  17353  fbunfip  17358  fgcl  17367  elfm2  17437  fmfnfmlem1  17443  fmco  17450  fbflim2  17466  flffbas  17484  cnpflf2  17489  flimfcls  17515  tmdgsum  17572  neibl  17841  metcnp3  17880  fgcfil  18491  caubl  18527  volsuplem  18706  ellimc3  19023  dvnadd  19072  dvnres  19074  cpnord  19078  dvnfre  19095  mpfrcl  19196  ply1divex  19316  aalioulem2  19507  cxpmul2  19838  wilthlem3  20074  lgsquad2lem2  20364  qabvexp  20541  gxnn0add  20702  gxnn0mul  20705  ismgm  20748  isexid2  20753  ipassi  21180  ubthlem2  21211  isch3  21582  shintcli  21669  shmodsi  21729  spansncvi  22010  pjjsi  22058  hoaddsub  22157  eigorthi  22178  pjss2coi  22505  pjnormssi  22509  pj3cor1i  22550  strb  22599  dmdmd  22641  mdsl0  22651  csmdsymi  22675  chrelat2i  22706  cvati  22707  mdsymlem3  22746  mdsymlem6  22749  sumdmdlem2  22760  dmdbr5ati  22763  cvmlift2lem1  22935  3ccased  23175  dedekind  23183  dfres3  23217  dfon2lem3  23240  rdgprc  23250  trpredmintr  23333  trpredrec  23340  wfr3g  23354  wfrlem12  23366  frr3g  23379  frrlem11  23392  sltval2  23408  axfelem13  23457  elfuns  23559  axcontlem4  23700  cgrextend  23736  btwndiff  23755  btwnconn1lem12  23826  brsegle  23836  broutsideof2  23850  funray  23868  meran1  23955  waj-ax  23958  arg-ax  23960  wl-pm2.86i  24026  isunscov  24170  restidsing  24172  twsymr  24174  prj1b  24175  prj3  24176  fixpc  24190  domintrefc  24222  mapmapmap  24245  injsurinj  24246  repfuntw  24257  cbcpcp  24259  prl  24264  prl2  24266  prjmapcp2  24267  dstr  24268  jidd  24289  midd  24290  int2pre  24334  ubpar  24358  inposet  24375  tolat  24383  toplat  24387  latdir  24392  ridlideq  24432  rzrlzreq  24433  resgcom  24448  grpodivone  24470  grpodivfo  24471  rltrran  24511  zerdivemp1  24533  muldisc  24578  svli2  24581  svs2  24584  truni1  24602  truni2  24603  truni3  24604  inttop2  24612  nsn  24627  intopcoaconlem3b  24635  intopcoaconc  24638  qusp  24639  intcont  24640  prcnt  24648  fisub  24651  cmptdst  24665  exopcopn  24669  prdnei  24670  limptlimpr2lem1  24671  limptlimpr2lem2  24672  islimrs  24677  islimrs3  24678  islimrs4  24679  bwt2  24689  iintlem1  24707  iint  24709  lvsovso  24723  supnuf  24726  claddrvr  24745  sigadd  24746  addcomv  24752  addcanrg  24764  negveudr  24766  subclrvd  24771  distsava  24786  intvconlem1  24800  hdrmp  24803  cmppfd  24842  domcmpd  24843  codcmpd  24844  cmpasso  24870  cmpida  24871  cmpidb  24872  cmpassoh  24898  homgrf  24899  imonclem  24910  cmpmon  24912  iepiclem  24920  isepic  24921  idfisf  24938  issrc  24964  propsrc  24965  partarelt1  24993  inttarcar  24998  fnctartar  25004  fnctartar2  25005  prismorcset2  25015  cmpmor  25072  setiscat  25076  lemindclsbu  25092  indcls2  25093  clscnc  25107  pgapspf2  25150  gltpntl  25169  lineval5a  25185  lineval6a  25186  isconcl5a  25198  isconcl5ab  25199  isconcl6a  25200  isibg2aa  25209  isib2g1a1  25213  isibg1a2  25214  isibg2a  25215  isibg1a3a  25219  isibg1a4a  25220  isibg1a5a  25221  bsstr  25225  nbssntr  25226  sgplpte21d  25233  segline  25238  pxysxy  25239  lppotoslem  25240  lppotos  25241  xsyysx  25242  nbssntrs  25244  pdiveql  25265  abhp  25270  elicc3  25325  nn0prpwlem  25335  nn0prpw  25336  fnessref  25390  neibastop2lem  25406  filnetlem4  25427  fzmul  25540  fdc  25552  seqpo  25554  incsequz  25555  isismty  25622  ismtybndlem  25627  heibor1lem  25630  ghomco  25670  zerdivemp1x  25683  pridlc  25793  ceqsex3OLD  25823  nelss  25848  incssnn0  25883  fphpd  25996  jm2.19lem3  26181  setindtr  26214  dfac21  26261  islssfg2  26266  mpaaeu  26452  psgnunilem4  26517  pm14.24  26730  hirstL-ax3  26782  sb5ALT  26904  truniALT  26921  onfrALTlem3  26925  ee223  27018  3orbi123VD  27191  sbc3orgVD  27192  exbirVD  27194  exbiriVD  27195  sbcim2gVD  27216  trsbcVD  27218  truniALTVD  27219  onfrALTlem3VD  27228  onfrALTlem2VD  27230  csbrngVD  27237  19.41rgVD  27243  a9e2eqVD  27248  a9e2ndeqVD  27250  2uasbanhVD  27252  sb5ALTVD  27254  vk15.4jVD  27255  ax12-3  27668  ax9lem2  27705  ax9lem5  27708  ax9lem15  27718  ax9vax9  27722  cdleme18d  29048  tendovalco  29518  cdlemn11pre  29964  dihord2pre  29979
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-mp 10
  Copyright terms: Public domain W3C validator