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  3072  orduniorsuc  4621  xpiindi  4821  dffv2  5592  fliftcnv  5810  unielxp  6158  dmtpos  6246  tpossym  6266  riotaprop  6328  oesuclem  6524  ercnv  6681  undom  6950  sucxpdom  7072  pwfilem  7150  rankr1id  7534  cardnn  7596  alephnbtwn2  7699  alephsucdom  7706  cdainflem  7817  isfin4-3  7941  axcclem  8083  infxpidm  8184  fpwwe2lem9  8260  gchpwdom  8296  elwina  8308  elina  8309  rankcf  8399  ltexprlem4  8663  lem1  9597  ltdivp1i  9683  rpnnen1lem5  10346  eluzfz1  10803  fzctr  10854  uznfz  10865  flid  10939  faclbnd3  11305  faclbnd4lem4  11309  bcn1  11325  hashfac  11396  sqrsq  11755  absrdbnd  11825  sqreulem  11843  sqreu  11844  gcd0id  12702  pcprod  12943  fldivp1  12945  invsym2  13665  pleval2i  14098  subrgsubm  15558  cncrng  16395  znchr  16516  tg1  16702  cldval  16760  cldss  16766  cldopn  16768  1stcrestlem  17178  regr1  17441  kqreg  17442  kqnrm  17443  ufilen  17625  symgtgp  17784  icoopnst  18437  cnheiborlem  18452  cfilfcls  18700  eflogeq  19955  logdivlt  19972  logdifbnd  20288  harmonicbnd4  20304  basellem5  20322  bposlem7  20529  chto1ub  20625  chpo1ub  20629  vmadivsum  20631  dchrmusum2  20643  dchrvmasum2if  20646  dchrvmasumlema  20649  dchrvmasumiflem2  20651  dchrisum0re  20662  dchrvmasumlem  20672  rplogsum  20676  mulogsumlem  20680  logdivsum  20682  selberg2lem  20699  pntrmax  20713  pntlem3  20758  pntleml  20760  pnt2  20762  issubgoi  20977  ismgm  20987  ismndo2  21012  ablomul  21022  rngomndo  21088  vcoprnelem  21134  hilablo  21739  mayete3i  22307  mayete3iOLD  22308  homulid2  22380  adjeu  22469  lnopeqi  22588  cnlnadjlem7  22653  adjbdlnb  22664  nmopcoadji  22681  bracnlnval  22694  derangen2  23116  subfaclim  23130  snmlff  23323  elfzm12  23419  relexp0  23436  relexpsucr  23437  relexp1  23438  relexpcnv  23440  relexpadd  23446  relexpindlem  23447  dfrtrclrec2  23451  rtrclreclem.trans  23454  rtrclreclem.min  23455  bpoly2  24203  areacirclem4  24339  areacirc  24343  alalifal  24415  islatalg  24595  isprsr  24636  glmrngo  24894  hmeogrpi  24948  limptlimpr2lem1  24986  islimrs4  24994  obsubc2  25262  idsubc  25263  domsubc  25264  codsubc  25265  cmpsubc  25268  lppotos  25556  refbas  25692  refssex  25693  fnetr  25698  prter3  26162  mzpsubmpt  26233  mzpnegmpt  26234  frgra1v  27538  uunT1  27928  atbase  28852  llnbase  29071  lplnbase  29096  lvolbase  29140  lhpbase  29560
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