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

Theorem mpancom 651
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 20 . 2  |-  ( ps 
->  ps )
3 mpancom.2 . 2  |-  ( (
ph  /\  ps )  ->  ch )
41, 2, 3syl2anc 643 1  |-  ( ps 
->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359
This theorem is referenced by:  mpan  652  spesbc  3202  orduniorsuc  4769  xpiindi  4969  dffv2  5755  fliftcnv  5992  unielxp  6344  dmtpos  6450  tpossym  6470  riotaprop  6532  oesuclem  6728  ercnv  6885  undom  7155  sucxpdom  7277  pwfilem  7359  rankr1id  7744  cardnn  7806  alephnbtwn2  7909  alephsucdom  7916  cdainflem  8027  isfin4-3  8151  axcclem  8293  infxpidm  8393  fpwwe2lem9  8469  gchpwdom  8505  elwina  8517  elina  8518  rankcf  8608  ltexprlem4  8872  lem1  9807  ltdivp1i  9893  rpnnen1lem5  10560  eluzfz1  11020  fzctr  11072  uznfz  11085  flid  11171  faclbnd3  11538  faclbnd4lem4  11542  bcn1  11559  hashfac  11662  sqrsq  12030  absrdbnd  12100  sqreulem  12118  sqreu  12119  gcd0id  12978  pcprod  13219  fldivp1  13221  invsym2  13943  pleval2i  14376  subrgsubm  15836  cncrng  16677  znchr  16798  tg1  16984  cldval  17042  cldss  17048  cldopn  17050  1stcrestlem  17468  regr1  17735  kqreg  17736  kqnrm  17737  ufilen  17915  symgtgp  18084  elrnust  18207  psmetdmdm  18289  metuvalOLD  18532  metuval  18533  icoopnst  18917  cnheiborlem  18932  cfilfcls  19180  eflogeq  20449  logdivlt  20469  logdifbnd  20785  harmonicbnd4  20802  basellem5  20820  bposlem7  21027  chto1ub  21123  chpo1ub  21127  vmadivsum  21129  dchrmusum2  21141  dchrvmasum2if  21144  dchrvmasumlema  21147  dchrvmasumiflem2  21149  dchrisum0re  21160  dchrvmasumlem  21170  rplogsum  21174  mulogsumlem  21178  logdivsum  21180  selberg2lem  21197  pntrmax  21211  pntlem3  21256  pntleml  21258  pnt2  21260  usgraidx2vlem2  21364  nbcusgra  21425  uvtxnbgravtx  21457  cusgrauvtxb  21458  wlkonprop  21485  wlkbprop  21487  trlonprop  21495  pthonprop  21530  spthonprp  21538  cyclispthon  21573  fargshiftfva  21579  constr3lem4  21587  constr3trllem2  21591  4cycl4dv  21607  eupatrl  21643  issubgoi  21851  ismgm  21861  ismndo2  21886  ablomul  21896  rngomndo  21962  vcoprnelem  22010  hilablo  22615  mayete3i  23183  mayete3iOLD  23184  homulid2  23256  adjeu  23345  lnopeqi  23464  cnlnadjlem7  23529  adjbdlnb  23540  nmopcoadji  23557  bracnlnval  23570  elunirn2  24016  dmct  24059  cnvct  24060  mptct  24062  mptctf  24065  xraddge02  24076  xrge0npcan  24169  metidval  24238  pstmval  24243  baselsiga  24451  sigasspw  24452  braew  24546  derangen2  24813  subfaclim  24827  snmlff  24969  elfzm12  25065  relexp0  25082  relexpsucr  25083  relexp1  25084  relexpcnv  25086  relexpadd  25091  relexpindlem  25092  dfrtrclrec2  25096  rtrclreclem.trans  25099  rtrclreclem.min  25100  fallfacfac  25302  bpoly2  26007  ismblfin  26146  itg2addnclem2  26156  areacirclem4  26183  areacirc  26187  refbas  26250  refssex  26251  fnetr  26256  prter3  26621  mzpsubmpt  26690  mzpnegmpt  26691  afveu  27884  3xpexg  27942  3xpfi  27967  usgra2pthspth  28035  usgra2adedgspthlem1  28043  usgra2adedgwlk  28046  2wlkonot  28062  2spthonot  28063  2spotfi  28089  frgra1v  28102  frgrancvvdeqlem3  28135  2spotmdisj  28171  uunT1  28601  atbase  29772  llnbase  29991  lplnbase  30016  lvolbase  30060  lhpbase  30480
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 178  df-an 361
  Copyright terms: Public domain W3C validator