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  1891  ax11b  1943  sb6rf  1986  sb56  1992  exsb  2093  mo  2140  exmoeu  2160  morimv  2166  eupickbi  2184  2mo  2196  2eu1  2198  exists2  2208  r19.12  2631  2gencl  2792  3gencl  2793  rcla4cv  2856  ceqex  2873  mob  2922  euind  2927  reuind  2943  2rmorex  2944  sseq2  3175  reupick2  3429  uneqdifeq  3517  difsn  3729  eqsn  3749  preq12b  3762  iinss2  3928  disjxiun  3994  trint0  4104  dtru  4173  sspwb  4195  copsexg  4224  pocl  4293  pofun  4302  solin  4309  frss  4332  tz7.7  4390  ordtri3  4400  ordtr2  4408  suc11  4468  onssneli  4474  reusv1  4506  reusv2lem1  4507  alxfr  4519  ralxfrALT  4525  iunpw  4542  ordom  4637  limom  4643  peano5  4651  2optocl  4753  3optocl  4754  ssrel  4764  ssrelrel  4775  relop  4822  asymref2  5048  xpidtr  5053  trin2  5054  sotri3  5061  poltletr  5066  xp11  5099  relcnvtr  5179  funmo  5210  fss  5335  fv3  5474  tz6.12-1  5477  tz6.12c  5481  tz6.12i  5482  mpteqb  5548  fornex  5684  funfvima  5687  fvclss  5694  f1fveq  5720  isoselem  5772  oprabid  5816  ovg  5920  poxp  6161  soxp  6162  tposfn2  6190  sorpsscmpl  6222  iotaval  6236  onnseq  6329  smoel  6345  smogt  6352  smoiso2  6354  tfrlem2  6360  tfr3  6383  tz7.48-2  6422  tz7.48-3  6424  tz7.49  6425  abianfp  6439  oecl  6504  oaordex  6524  oalimcl  6526  oaass  6527  omordi  6532  omlimcl  6544  odi  6545  omeulem1  6548  oen0  6552  oewordri  6558  nnawordi  6587  nnaass  6588  nnmordi  6597  omabs  6613  omsmolem  6619  iiner  6699  2ecoptocl  6717  3ecoptocl  6718  th3qlem2  6733  undifixp  6820  xpdom2  6925  xpf1o  6991  infensuc  7007  php  7013  onomeneq  7018  isinf  7044  findcard2  7066  unblem2  7078  finsschain  7130  marypha1  7155  hartogs  7227  card2on  7236  card2inf  7237  xpwdomg  7267  elirrv  7279  inf3lem1  7297  inf3lem2  7298  inf3lem3  7299  inf3lem5  7301  noinfep  7328  noinfepOLD  7329  trcl  7378  en3lp  7386  tcel  7398  r1sdom  7414  rankonidlem  7468  scottex  7523  pr2ne  7603  dif1card  7606  fodomnum  7652  cardaleph  7684  kmlem4  7747  kmlem9  7752  kmlem12  7755  kmlem13  7756  cflim2  7857  cfsmolem  7864  infpssrlem3  7899  isfin7-2  7990  fin1a2lem6  7999  fin1a2lem10  8003  fin1a2lem12  8005  domtriomlem  8036  axdc3lem4  8047  axdc4lem  8049  zorn2lem3  8093  zorn2lem4  8094  zorn2lem5  8095  zorn2lem6  8096  zorn2lem7  8097  zornn0g  8100  axdclem  8114  axdclem2  8115  ondomon  8153  alephval2  8162  cfpwsdom  8174  wunr1om  8309  wuncval2  8337  tskr1om  8357  grupr  8387  gruiun  8389  ingru  8405  grothomex  8419  indpi  8499  nqereu  8521  genpnnp  8597  prlem934  8625  ltaddpr2  8627  reclem2pr  8640  mulgt0sr  8695  supsrlem  8701  lemul1a  9578  squeeze0  9627  peano5nni  9717  nnunb  9929  fzind  10077  nn0ind-raph  10080  zindd  10081  eluzadd  10224  uzin  10228  xmulasslem  10572  icoshft  10725  fzen  10778  expcllem  11081  expeq0  11099  mulexp  11108  leexp2r  11126  bernneq  11194  facdiv  11267  hashmap  11353  cjexp  11601  absexp  11755  iseraltlem2  12121  sin01gt0  12433  alzdvds  12541  dvdslegcd  12658  gcdneg  12668  rplpwr  12698  qredeq  12748  prmpwdvds  12914  prmreclem4  12929  ramcl  13039  imasleval  13406  mreiincl  13461  mreexexd  13513  drsdirfi  14035  spwmo  14298  efgi2  14997  fiinopn  16610  tgcl  16670  distop  16696  isclo2  16788  iscldtop  16795  ssnei2  16816  opnnei  16820  pnfnei  16913  mnfnei  16914  tgcnp  16946  cnpnei  16956  2ndcctbss  17144  1stcelcls  17150  txcnpi  17265  cnmptcom  17335  fbfinnfr  17499  isfildlem  17515  snfil  17522  fbunfip  17527  fgcl  17536  elfm2  17606  fmfnfmlem1  17612  fmco  17619  fbflim2  17635  flffbas  17653  cnpflf2  17658  flimfcls  17684  tmdgsum  17741  neibl  18010  metcnp3  18049  fgcfil  18660  caubl  18696  volsuplem  18875  ellimc3  19192  dvnadd  19241  dvnres  19243  cpnord  19247  dvnfre  19264  mpfrcl  19365  ply1divex  19485  aalioulem2  19676  cxpmul2  19999  wilthlem3  20271  lgsquad2lem2  20561  qabvexp  20738  gxnn0add  20902  gxnn0mul  20905  ismgm  20948  isexid2  20953  ipassi  21380  ubthlem2  21411  isch3  21782  shintcli  21869  shmodsi  21929  spansncvi  22192  pjjsi  22240  hoaddsub  22357  eigorthi  22378  pjss2coi  22705  pjnormssi  22709  pj3cor1i  22750  strb  22799  dmdmd  22841  mdsl0  22851  csmdsymi  22875  chrelat2i  22906  cvati  22907  mdsymlem3  22946  mdsymlem6  22949  sumdmdlem2  22960  dmdbr5ati  22963  cvmlift2lem1  23206  3ccased  23446  dedekind  23454  dfres3  23488  dfon2lem3  23511  rdgprc  23521  trpredmintr  23604  trpredrec  23611  wfr3g  23625  wfrlem12  23637  frr3g  23650  frrlem11  23663  sltval2  23679  axfelem13  23728  elfuns  23830  axcontlem4  23971  cgrextend  24007  btwndiff  24026  btwnconn1lem12  24097  brsegle  24107  broutsideof2  24121  funray  24139  meran1  24226  waj-ax  24229  arg-ax  24231  wl-pm2.86i  24297  isunscov  24441  restidsing  24443  twsymr  24445  prj1b  24446  prj3  24447  fixpc  24461  domintrefc  24493  mapmapmap  24516  injsurinj  24517  repfuntw  24528  cbcpcp  24530  prl  24535  prl2  24537  prjmapcp2  24538  dstr  24539  jidd  24560  midd  24561  int2pre  24605  ubpar  24629  inposet  24646  tolat  24654  toplat  24658  latdir  24663  ridlideq  24703  rzrlzreq  24704  resgcom  24719  grpodivone  24741  grpodivfo  24742  rltrran  24782  zerdivemp1  24804  muldisc  24849  svli2  24852  svs2  24855  truni1  24873  truni2  24874  truni3  24875  inttop2  24883  nsn  24898  intopcoaconlem3b  24906  intopcoaconc  24909  qusp  24910  intcont  24911  prcnt  24919  fisub  24922  cmptdst  24936  exopcopn  24940  prdnei  24941  limptlimpr2lem1  24942  limptlimpr2lem2  24943  islimrs  24948  islimrs3  24949  islimrs4  24950  bwt2  24960  iintlem1  24978  iint  24980  lvsovso  24994  supnuf  24997  claddrvr  25016  sigadd  25017  addcomv  25023  addcanrg  25035  negveudr  25037  subclrvd  25042  distsava  25057  intvconlem1  25071  hdrmp  25074  cmppfd  25113  domcmpd  25114  codcmpd  25115  cmpasso  25141  cmpida  25142  cmpidb  25143  cmpassoh  25169  homgrf  25170  imonclem  25181  cmpmon  25183  iepiclem  25191  isepic  25192  idfisf  25209  issrc  25235  propsrc  25236  partarelt1  25264  inttarcar  25269  fnctartar  25275  fnctartar2  25276  prismorcset2  25286  cmpmor  25343  setiscat  25347  lemindclsbu  25363  indcls2  25364  clscnc  25378  pgapspf2  25421  gltpntl  25440  lineval5a  25456  lineval6a  25457  isconcl5a  25469  isconcl5ab  25470  isconcl6a  25471  isibg2aa  25480  isib2g1a1  25484  isibg1a2  25485  isibg2a  25486  isibg1a3a  25490  isibg1a4a  25491  isibg1a5a  25492  bsstr  25496  nbssntr  25497  sgplpte21d  25504  segline  25509  pxysxy  25510  lppotoslem  25511  lppotos  25512  xsyysx  25513  nbssntrs  25515  pdiveql  25536  abhp  25541  elicc3  25596  nn0prpwlem  25606  nn0prpw  25607  fnessref  25661  neibastop2lem  25677  filnetlem4  25698  fzmul  25811  fdc  25823  seqpo  25825  incsequz  25826  isismty  25893  ismtybndlem  25898  heibor1lem  25901  ghomco  25941  zerdivemp1x  25954  pridlc  26064  ceqsex3OLD  26094  nelss  26119  incssnn0  26154  fphpd  26267  jm2.19lem3  26452  setindtr  26485  dfac21  26532  islssfg2  26537  mpaaeu  26723  psgnunilem4  26788  pm14.24  27001  stoweidlem26  27144  hirstL-ax3  27209  rexsb  27295  rexrsb  27296  2reu1  27313  sb5ALT  27424  truniALT  27441  onfrALTlem3  27445  ee223  27539  3orbi123VD  27759  sbc3orgVD  27760  exbirVD  27762  exbiriVD  27763  sbcim2gVD  27784  trsbcVD  27786  truniALTVD  27787  onfrALTlem3VD  27796  onfrALTlem2VD  27798  csbrngVD  27805  19.41rgVD  27811  a9e2eqVD  27816  a9e2ndeqVD  27818  2uasbanhVD  27820  sb5ALTVD  27822  vk15.4jVD  27823  equequ2K  28238  a4eimfK  28247  a4imfK  28248  a4imK  28249  a4imvK  28250  ax12olem21K  28321  ax12olem21X  28322  ax12olem22K  28324  ax12olem23aK  28326  ax12olem23X  28327  ax10lem16X  28335  ax10lem26X  28345  ax10X  28347  ax12-3  28354  ax9lem2  28391  ax9lem5  28394  ax9lem15  28404  ax9vax9  28408  cdleme18d  29734  tendovalco  30204  cdlemn11pre  30650  dihord2pre  30665
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-mp 10
  Copyright terms: Public domain W3C validator