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

Theorem mpancom 650
Description: An inference based on modus ponens with commutation of antecedents. (Contributed by NM, 28-Oct-2003.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
Hypotheses
Ref Expression
mpancom.1  |-  ( ps 
->  ph )
mpancom.2  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
mpancom  |-  ( ps 
->  ch )

Proof of Theorem mpancom
StepHypRef Expression
1 mpancom.1 . 2  |-  ( ps 
->  ph )
2 id 19 . 2  |-  ( ps 
->  ps )
3 mpancom.2 . 2  |-  ( (
ph  /\  ps )  ->  ch )
41, 2, 3syl2anc 642 1  |-  ( ps 
->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  mpan  651  spesbc  3085  orduniorsuc  4637  xpiindi  4837  dffv2  5608  fliftcnv  5826  unielxp  6174  dmtpos  6262  tpossym  6282  riotaprop  6344  oesuclem  6540  ercnv  6697  undom  6966  sucxpdom  7088  pwfilem  7166  rankr1id  7550  cardnn  7612  alephnbtwn2  7715  alephsucdom  7722  cdainflem  7833  isfin4-3  7957  axcclem  8099  infxpidm  8200  fpwwe2lem9  8276  gchpwdom  8312  elwina  8324  elina  8325  rankcf  8415  ltexprlem4  8679  lem1  9613  ltdivp1i  9699  rpnnen1lem5  10362  eluzfz1  10819  fzctr  10870  uznfz  10881  flid  10955  faclbnd3  11321  faclbnd4lem4  11325  bcn1  11341  hashfac  11412  sqrsq  11771  absrdbnd  11841  sqreulem  11859  sqreu  11860  gcd0id  12718  pcprod  12959  fldivp1  12961  invsym2  13681  pleval2i  14114  subrgsubm  15574  cncrng  16411  znchr  16532  tg1  16718  cldval  16776  cldss  16782  cldopn  16784  1stcrestlem  17194  regr1  17457  kqreg  17458  kqnrm  17459  ufilen  17641  symgtgp  17800  icoopnst  18453  cnheiborlem  18468  cfilfcls  18716  eflogeq  19971  logdivlt  19988  logdifbnd  20304  harmonicbnd4  20320  basellem5  20338  bposlem7  20545  chto1ub  20641  chpo1ub  20645  vmadivsum  20647  dchrmusum2  20659  dchrvmasum2if  20662  dchrvmasumlema  20665  dchrvmasumiflem2  20667  dchrisum0re  20678  dchrvmasumlem  20688  rplogsum  20692  mulogsumlem  20696  logdivsum  20698  selberg2lem  20715  pntrmax  20729  pntlem3  20774  pntleml  20776  pnt2  20778  issubgoi  20993  ismgm  21003  ismndo2  21028  ablomul  21038  rngomndo  21104  vcoprnelem  21150  hilablo  21755  mayete3i  22323  mayete3iOLD  22324  homulid2  22396  adjeu  22485  lnopeqi  22604  cnlnadjlem7  22669  adjbdlnb  22680  nmopcoadji  22697  bracnlnval  22710  elunirn2  23230  xraddge02  23267  xrge0npcan  23348  dmct  23357  cnvct  23358  mptct  23360  mptctf  23363  baselsiga  23491  sigasspw  23492  derangen2  23720  subfaclim  23734  snmlff  23927  elfzm12  24023  relexp0  24040  relexpsucr  24041  relexp1  24042  relexpcnv  24044  relexpadd  24050  relexpindlem  24051  dfrtrclrec2  24055  rtrclreclem.trans  24058  rtrclreclem.min  24059  bpoly2  24864  itg2addnclem2  25004  areacirclem4  25030  areacirc  25034  alalifal  25106  islatalg  25286  isprsr  25327  glmrngo  25585  hmeogrpi  25639  limptlimpr2lem1  25677  islimrs4  25685  obsubc2  25953  idsubc  25954  domsubc  25955  codsubc  25956  cmpsubc  25959  lppotos  26247  refbas  26383  refssex  26384  fnetr  26389  prter3  26853  mzpsubmpt  26924  mzpnegmpt  26925  afveu  28121  nbcusgra  28298  uvtxnbgravtx  28308  wlkbprop  28333  trlonprop  28341  cyclispthon  28378  fargshiftfva  28384  eupatrl  28385  constr3lem4  28393  constr3trllem2  28397  4cycl4dv  28413  frgra1v  28422  uunT1  28869  atbase  30101  llnbase  30320  lplnbase  30345  lvolbase  30389  lhpbase  30809
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator