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  2618  2gencl  2755  3gencl  2756  rcla4cv  2818  ceqex  2835  mob  2884  euind  2889  reuind  2903  sseq2  3121  reupick2  3361  uneqdifeq  3448  difsn  3657  eqsn  3675  preq12b  3688  iinss2  3852  disjxiun  3917  trint0  4027  dtru  4095  sspwb  4117  copsexg  4145  pocl  4214  pofun  4223  solin  4230  frss  4253  tz7.7  4311  ordtri3  4321  ordtr2  4329  suc11  4387  onssneli  4393  reusv1  4425  reusv2lem1  4426  alxfr  4438  ralxfrALT  4444  iunpw  4461  ordom  4556  limom  4562  peano5  4570  2optocl  4672  3optocl  4673  ssrel  4683  ssrelrel  4694  relop  4741  asymref2  4967  xpidtr  4972  trin2  4973  sotri3  4980  poltletr  4985  xp11  5018  relcnvtr  5098  funmo  5129  fss  5254  fv3  5393  tz6.12-1  5396  tz6.12c  5400  tz6.12i  5401  mpteqb  5466  fornex  5602  funfvima  5605  fvclss  5612  f1fveq  5638  isoselem  5690  oprabid  5734  ovg  5838  poxp  6079  soxp  6080  tposfn2  6108  sorpsscmpl  6140  iotaval  6154  onnseq  6247  smoel  6263  smogt  6270  smoiso2  6272  tfrlem2  6278  tfr3  6301  tz7.48-2  6340  tz7.48-3  6342  tz7.49  6343  abianfp  6357  oecl  6422  oaordex  6442  oalimcl  6444  oaass  6445  omordi  6450  omlimcl  6462  odi  6463  omeulem1  6466  oen0  6470  oewordri  6476  nnawordi  6505  nnaass  6506  nnmordi  6515  omabs  6531  omsmolem  6537  iiner  6617  2ecoptocl  6635  3ecoptocl  6636  th3qlem2  6651  undifixp  6738  xpdom2  6842  xpf1o  6908  infensuc  6924  php  6930  onomeneq  6935  isinf  6961  findcard2  6983  unblem2  6995  finsschain  7046  marypha1  7071  hartogs  7143  card2on  7152  card2inf  7153  xpwdomg  7183  elirrv  7195  inf3lem1  7213  inf3lem2  7214  inf3lem3  7215  inf3lem5  7217  noinfep  7244  noinfepOLD  7245  trcl  7294  en3lp  7302  tcel  7314  r1sdom  7330  rankonidlem  7384  scottex  7439  pr2ne  7519  dif1card  7522  fodomnum  7568  cardaleph  7600  kmlem4  7663  kmlem9  7668  kmlem12  7671  kmlem13  7672  cflim2  7773  cfsmolem  7780  infpssrlem3  7815  isfin7-2  7906  fin1a2lem6  7915  fin1a2lem10  7919  fin1a2lem12  7921  domtriomlem  7952  axdc3lem4  7963  axdc4lem  7965  zorn2lem3  8009  zorn2lem4  8010  zorn2lem5  8011  zorn2lem6  8012  zorn2lem7  8013  zornn0g  8016  axdclem  8030  axdclem2  8031  ondomon  8067  alephval2  8074  cfpwsdom  8086  wunr1om  8221  wuncval2  8249  tskr1om  8269  grupr  8299  gruiun  8301  ingru  8317  grothomex  8331  indpi  8411  nqereu  8433  genpnnp  8509  prlem934  8537  ltaddpr2  8539  reclem2pr  8552  mulgt0sr  8607  supsrlem  8613  lemul1a  9490  squeeze0  9539  peano5nni  9629  nnunb  9840  fzind  9988  nn0ind-raph  9991  zindd  9992  eluzadd  10135  uzin  10139  xmulasslem  10483  icoshft  10636  fzen  10689  expcllem  10992  expeq0  11010  mulexp  11019  leexp2r  11037  bernneq  11105  facdiv  11178  hashmap  11264  cjexp  11512  absexp  11666  iseraltlem2  12032  sin01gt0  12344  alzdvds  12452  dvdslegcd  12569  gcdneg  12579  rplpwr  12609  qredeq  12659  prmpwdvds  12825  prmreclem4  12840  ramcl  12950  imasleval  13317  mreiincl  13370  drsdirfi  13916  spwmo  14170  efgi2  14869  fiinopn  16479  tgcl  16539  distop  16565  isclo2  16657  iscldtop  16664  ssnei2  16685  opnnei  16689  pnfnei  16782  mnfnei  16783  tgcnp  16815  cnpnei  16825  2ndcctbss  17013  1stcelcls  17019  txcnpi  17134  cnmptcom  17204  fbfinnfr  17368  isfildlem  17384  snfil  17391  fbunfip  17396  fgcl  17405  elfm2  17475  fmfnfmlem1  17481  fmco  17488  fbflim2  17504  flffbas  17522  cnpflf2  17527  flimfcls  17553  tmdgsum  17610  neibl  17879  metcnp3  17918  fgcfil  18529  caubl  18565  volsuplem  18744  ellimc3  19061  dvnadd  19110  dvnres  19112  cpnord  19116  dvnfre  19133  mpfrcl  19234  ply1divex  19354  aalioulem2  19545  cxpmul2  19904  wilthlem3  20140  lgsquad2lem2  20430  qabvexp  20607  gxnn0add  20771  gxnn0mul  20774  ismgm  20817  isexid2  20822  ipassi  21249  ubthlem2  21280  isch3  21651  shintcli  21738  shmodsi  21798  spansncvi  22079  pjjsi  22127  hoaddsub  22226  eigorthi  22247  pjss2coi  22574  pjnormssi  22578  pj3cor1i  22619  strb  22668  dmdmd  22710  mdsl0  22720  csmdsymi  22744  chrelat2i  22775  cvati  22776  mdsymlem3  22815  mdsymlem6  22818  sumdmdlem2  22829  dmdbr5ati  22832  cvmlift2lem1  23004  3ccased  23244  dedekind  23252  dfres3  23286  dfon2lem3  23309  rdgprc  23319  trpredmintr  23402  trpredrec  23409  wfr3g  23423  wfrlem12  23435  frr3g  23448  frrlem11  23461  sltval2  23477  axfelem13  23526  elfuns  23628  axcontlem4  23769  cgrextend  23805  btwndiff  23824  btwnconn1lem12  23895  brsegle  23905  broutsideof2  23919  funray  23937  meran1  24024  waj-ax  24027  arg-ax  24029  wl-pm2.86i  24095  isunscov  24239  restidsing  24241  twsymr  24243  prj1b  24244  prj3  24245  fixpc  24259  domintrefc  24291  mapmapmap  24314  injsurinj  24315  repfuntw  24326  cbcpcp  24328  prl  24333  prl2  24335  prjmapcp2  24336  dstr  24337  jidd  24358  midd  24359  int2pre  24403  ubpar  24427  inposet  24444  tolat  24452  toplat  24456  latdir  24461  ridlideq  24501  rzrlzreq  24502  resgcom  24517  grpodivone  24539  grpodivfo  24540  rltrran  24580  zerdivemp1  24602  muldisc  24647  svli2  24650  svs2  24653  truni1  24671  truni2  24672  truni3  24673  inttop2  24681  nsn  24696  intopcoaconlem3b  24704  intopcoaconc  24707  qusp  24708  intcont  24709  prcnt  24717  fisub  24720  cmptdst  24734  exopcopn  24738  prdnei  24739  limptlimpr2lem1  24740  limptlimpr2lem2  24741  islimrs  24746  islimrs3  24747  islimrs4  24748  bwt2  24758  iintlem1  24776  iint  24778  lvsovso  24792  supnuf  24795  claddrvr  24814  sigadd  24815  addcomv  24821  addcanrg  24833  negveudr  24835  subclrvd  24840  distsava  24855  intvconlem1  24869  hdrmp  24872  cmppfd  24911  domcmpd  24912  codcmpd  24913  cmpasso  24939  cmpida  24940  cmpidb  24941  cmpassoh  24967  homgrf  24968  imonclem  24979  cmpmon  24981  iepiclem  24989  isepic  24990  idfisf  25007  issrc  25033  propsrc  25034  partarelt1  25062  inttarcar  25067  fnctartar  25073  fnctartar2  25074  prismorcset2  25084  cmpmor  25141  setiscat  25145  lemindclsbu  25161  indcls2  25162  clscnc  25176  pgapspf2  25219  gltpntl  25238  lineval5a  25254  lineval6a  25255  isconcl5a  25267  isconcl5ab  25268  isconcl6a  25269  isibg2aa  25278  isib2g1a1  25282  isibg1a2  25283  isibg2a  25284  isibg1a3a  25288  isibg1a4a  25289  isibg1a5a  25290  bsstr  25294  nbssntr  25295  sgplpte21d  25302  segline  25307  pxysxy  25308  lppotoslem  25309  lppotos  25310  xsyysx  25311  nbssntrs  25313  pdiveql  25334  abhp  25339  elicc3  25394  nn0prpwlem  25404  nn0prpw  25405  fnessref  25459  neibastop2lem  25475  filnetlem4  25496  fzmul  25609  fdc  25621  seqpo  25623  incsequz  25624  isismty  25691  ismtybndlem  25696  heibor1lem  25699  ghomco  25739  zerdivemp1x  25752  pridlc  25862  ceqsex3OLD  25892  nelss  25917  incssnn0  25952  fphpd  26065  jm2.19lem3  26250  setindtr  26283  dfac21  26330  islssfg2  26335  mpaaeu  26521  psgnunilem4  26586  pm14.24  26799  hirstL-ax3  26851  sb5ALT  26981  truniALT  26998  onfrALTlem3  27002  ee223  27096  3orbi123VD  27316  sbc3orgVD  27317  exbirVD  27319  exbiriVD  27320  sbcim2gVD  27341  trsbcVD  27343  truniALTVD  27344  onfrALTlem3VD  27353  onfrALTlem2VD  27355  csbrngVD  27362  19.41rgVD  27368  a9e2eqVD  27373  a9e2ndeqVD  27375  2uasbanhVD  27377  sb5ALTVD  27379  vk15.4jVD  27380  ax12-3  27793  ax9lem2  27830  ax9lem5  27833  ax9lem15  27843  ax9vax9  27847  cdleme18d  29173  tendovalco  29643  cdlemn11pre  30089  dihord2pre  30104
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-mp 10
  Copyright terms: Public domain W3C validator