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

Theorem mpancom 669
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 22 . 2  |-  ( ps 
->  ps )
3 mpancom.2 . 2  |-  ( (
ph  /\  ps )  ->  ch )
41, 2, 3syl2anc 661 1  |-  ( ps 
->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  mpan  670  spesbc  3404  xpiindi  5124  fununfun  5618  dffv2  5927  fliftcnv  6190  riotaprop  6262  elovmpt3rab1  6517  3xpexg  6584  orduniorsuc  6646  unielxp  6817  dmtpos  6965  tpossym  6985  oesuclem  7173  ercnv  7330  undom  7603  sucxpdom  7727  3xpfi  7790  pwfilem  7812  rankr1id  8278  cardnn  8342  alephnbtwn2  8451  alephsucdom  8458  cdainflem  8569  isfin4-3  8693  axcclem  8835  infxpidm  8935  fpwwe2lem9  9014  gchpwdom  9046  elwina  9062  elina  9063  rankcf  9153  ltexprlem4  9415  lem1  10384  ltdivp1i  10473  rpnnen1lem5  11216  eluzfz1  11697  fzpred  11732  uznfz  11765  fz0fzdiffz0  11786  fzctr  11790  flid  11919  modid0  11995  2txmodxeq0  12021  faclbnd3  12344  faclbnd4lem4  12348  bcn1  12365  hashfac  12481  hash2prv  12499  hash2sspr  12500  repswsymballbi  12726  wrdlen2i  12858  sqrtsq  13077  absrdbnd  13148  sqreulem  13166  sqreu  13167  gcd0id  14033  pcprod  14286  fldivp1  14288  invsym2  15029  pleval2i  15463  subrgsubm  17310  cncrng  18307  znchr  18468  mattposvs  18824  smadiadetglem2  19041  tg1  19332  cldval  19390  cldss  19396  cldopn  19398  1stcrestlem  19819  refbas  19877  refssex  19878  regr1  20117  kqreg  20118  kqnrm  20119  ufilen  20297  symgtgp  20466  elrnust  20593  psmetdmdm  20675  metuvalOLD  20918  metuval  20919  icoopnst  21305  cnheiborlem  21320  cfilfcls  21579  eflogeq  22851  logdivlt  22871  logdifbnd  23188  harmonicbnd4  23205  basellem5  23223  bposlem7  23430  chto1ub  23526  chpo1ub  23530  vmadivsum  23532  dchrmusum2  23544  dchrvmasum2if  23547  dchrvmasumlema  23550  dchrvmasumiflem2  23552  dchrisum0re  23563  dchrvmasumlem  23573  rplogsum  23577  mulogsumlem  23581  logdivsum  23583  selberg2lem  23600  pntrmax  23614  pntlem3  23659  pntleml  23661  pnt2  23663  usgraidx2vlem2  24257  nbcusgra  24328  uvtxnbgravtx  24360  cusgrauvtxb  24361  wlkbprop  24388  wlkonprop  24400  trlonprop  24409  pthonprop  24444  spthonprp  24452  usgra2adedgspthlem1  24476  usgra2adedgwlk  24479  cyclispthon  24498  fargshiftfva  24504  constr3lem4  24512  constr3trllem2  24516  4cycl4dv  24532  wlklniswwlkn1  24564  clwlkiswlk  24622  clwwlkf  24659  wwlkext2clwwlk  24668  erclwwlknsym  24691  erclwwlkntr  24692  clwlkfclwwlk  24709  eupatrl  24833  frgra1v  24863  frgrancvvdeqlem3  24897  numclwlk1lem2fo  24960  numclwlk2lem2f  24968  numclwwlk5lem  24976  issubgoi  25177  ismgmOLD  25187  ismndo2  25212  ablomul  25222  rngomndo  25288  vcoprnelem  25336  hilablo  25942  mayete3i  26511  mayete3iOLD  26512  homulid2  26584  adjeu  26673  lnopeqi  26792  cnlnadjlem7  26857  adjbdlnb  26868  nmopcoadji  26885  bracnlnval  26898  elunirn2  27354  dmct  27402  cnvct  27403  mptct  27406  mptctf  27409  xraddge02  27442  xrge0npcan  27550  gsumle  27636  gsumvsca1  27639  gsumvsca2  27640  metidval  27735  pstmval  27740  baselsiga  27981  sigasspw  27982  ddeval1  28072  ddeval0  28073  braew  28080  derangen2  28484  subfaclim  28498  snmlff  28640  elfzm12  28907  relexp0  28918  relexpsucr  28919  relexp1  28920  relexpcnv  28922  relexpadd  28927  relexpindlem  28928  dfrtrclrec2  28932  rtrclreclem.trans  28935  rtrclreclem.min  28936  bpoly2  29787  wl-sbal1  29981  ismblfin  30023  itg2addnclem2  30035  areacirclem2  30076  areacirc  30080  fnetr  30137  prter3  30591  mzpsubmpt  30643  mzpnegmpt  30644  lcmgcdlem  31181  afveu  32072  usgra2pthspth  32185  lindsrng01  32779  uunT1  33285  atbase  34716  llnbase  34935  lplnbase  34960  lvolbase  35004  lhpbase  35424
  Copyright terms: Public domain W3C validator